Metamath Proof Explorer

Theorem nd3

Description: A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002)

Ref Expression
Assertion nd3 
|- ( A. x x = y -> -. A. z x e. y )

Proof

Step Hyp Ref Expression
1 elirrv 
 |-  -. x e. x
2 elequ2 
 |-  ( x = y -> ( x e. x <-> x e. y ) )
3 1 2 mtbii 
 |-  ( x = y -> -. x e. y )
4 3 sps 
 |-  ( A. x x = y -> -. x e. y )
5 sp 
 |-  ( A. z x e. y -> x e. y )
6 4 5 nsyl 
 |-  ( A. x x = y -> -. A. z x e. y )