Theorem nd2

Description: A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Jan-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	nd2	$$⊢\forall xx=y\to \neg \forall xz\in y$$

Proof

Step	Hyp	Ref	Expression
1		elirrv	$$⊢\neg z\in z$$
2		stdpc4	$$⊢\forall yz\in y\to \left[z/y\right]z\in y$$
3	1	nfnth	$$⊢Ⅎyz\in z$$
4		elequ2	$$⊢y=z\to \left(z\in y\leftrightarrow z\in z\right)$$
5	3 4	sbie	$$⊢\left[z/y\right]z\in y\leftrightarrow z\in z$$
6	2 5	sylib	$$⊢\forall yz\in y\to z\in z$$
7	1 6	mto	$$⊢\neg \forall yz\in y$$
8		axc11	$$⊢\forall xx=y\to \left(\forall xz\in y\to \forall yz\in y\right)$$
9	7 8	mtoi	$$⊢\forall xx=y\to \neg \forall xz\in y$$