Theorem dveel2

Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)

Conclusion

\( \vdash \neg \forall x \, x = y \rightarrow z' \in y \rightarrow \forall x \, z' \in y \)

Proof

elequ2

\( \vdash w = y \rightarrow (z' \in w \leftrightarrow z' \in y) \)

dvelimv _