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

Proof

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