Theorem dveel1

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 y \in z' \rightarrow \forall x \, y \in z' \)

Proof

elequ1

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

dvelimv _