This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axextnd

Description: A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-Aug-2003) (New usage is discouraged.)

Ref Expression
Assertion axextnd 
|- E. x ( ( x e. y <-> x e. z ) -> y = z )

Proof

Step Hyp Ref Expression
1 nfnae 
 |-  F/ x -. A. x x = y
2 nfnae 
 |-  F/ x -. A. x x = z
3 1 2 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
4 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
5 4 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x y )
6 5 nfcrd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. y )
7 nfcvf 
 |-  ( -. A. x x = z -> F/_ x z )
8 7 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x z )
9 8 nfcrd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. z )
10 6 9 nfbid 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w e. y <-> w e. z ) )
11 elequ1 
 |-  ( w = x -> ( w e. y <-> x e. y ) )
12 elequ1 
 |-  ( w = x -> ( w e. z <-> x e. z ) )
13 11 12 bibi12d 
 |-  ( w = x -> ( ( w e. y <-> w e. z ) <-> ( x e. y <-> x e. z ) ) )
14 13 a1i 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( w e. y <-> w e. z ) <-> ( x e. y <-> x e. z ) ) ) )
15 3 10 14 cbvald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. w ( w e. y <-> w e. z ) <-> A. x ( x e. y <-> x e. z ) ) )
16 axextg 
 |-  ( A. w ( w e. y <-> w e. z ) -> y = z )
17 15 16 biimtrrdi 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. x ( x e. y <-> x e. z ) -> y = z ) )
18 19.8a 
 |-  ( y = z -> E. x y = z )
19 17 18 syl6 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. x ( x e. y <-> x e. z ) -> E. x y = z ) )
20 19 ex 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> ( A. x ( x e. y <-> x e. z ) -> E. x y = z ) ) )
21 ax6e 
 |-  E. x x = z
22 ax7 
 |-  ( x = y -> ( x = z -> y = z ) )
23 22 aleximi 
 |-  ( A. x x = y -> ( E. x x = z -> E. x y = z ) )
24 21 23 mpi 
 |-  ( A. x x = y -> E. x y = z )
25 24 a1d 
 |-  ( A. x x = y -> ( A. x ( x e. y <-> x e. z ) -> E. x y = z ) )
26 ax6e 
 |-  E. x x = y
27 ax7 
 |-  ( x = z -> ( x = y -> z = y ) )
28 equcomi 
 |-  ( z = y -> y = z )
29 27 28 syl6 
 |-  ( x = z -> ( x = y -> y = z ) )
30 29 aleximi 
 |-  ( A. x x = z -> ( E. x x = y -> E. x y = z ) )
31 26 30 mpi 
 |-  ( A. x x = z -> E. x y = z )
32 31 a1d 
 |-  ( A. x x = z -> ( A. x ( x e. y <-> x e. z ) -> E. x y = z ) )
33 20 25 32 pm2.61ii 
 |-  ( A. x ( x e. y <-> x e. z ) -> E. x y = z )
34 33 19.35ri 
 |-  E. x ( ( x e. y <-> x e. z ) -> y = z )