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	|- ( A. x x = y -> -. A. x y e. z )

Proof

Step	Hyp	Ref	Expression
1		elirrv	|- -. z e. z
2		stdpc4	|- ( A. y y e. z -> [ z / y ] y e. z )
3	1	nfnth	|- F/ y z e. z
4		elequ1	|- ( y = z -> ( y e. z <-> z e. z ) )
5	3 4	sbie	|- ( [ z / y ] y e. z <-> z e. z )
6	2 5	sylib	|- ( A. y y e. z -> z e. z )
7	1 6	mto	|- -. A. y y e. z
8		axc11	|- ( A. x x = y -> ( A. x y e. z -> A. y y e. z ) )
9	7 8	mtoi	|- ( A. x x = y -> -. A. x y e. z )