Metamath Proof Explorer

Theorem axextbdist

Description: axextb with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010)

Ref Expression
Assertion axextbdist 
|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y <-> A. z ( z e. x <-> z e. y ) ) )

Proof

Step Hyp Ref Expression
1 axc9 
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
2 1 imp 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> A. z x = y ) )
3 nfnae 
 |-  F/ z -. A. z z = x
4 nfnae 
 |-  F/ z -. A. z z = y
5 3 4 nfan 
 |-  F/ z ( -. A. z z = x /\ -. A. z z = y )
6 elequ2 
 |-  ( x = y -> ( z e. x <-> z e. y ) )
7 6 a1i 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> ( z e. x <-> z e. y ) ) )
8 5 7 alimd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. z x = y -> A. z ( z e. x <-> z e. y ) ) )
9 2 8 syld 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> A. z ( z e. x <-> z e. y ) ) )
10 axextdist 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. z ( z e. x <-> z e. y ) -> x = y ) )
11 9 10 impbid 
 |-  ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y <-> A. z ( z e. x <-> z e. y ) ) )