Theorem nd1

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	nd1	$$⊢\forall xx=y\to \neg \forall xy\in z$$

Proof

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