Metamath Proof Explorer

Theorem axunnd

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

Ref Expression
Assertion axunnd 
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )

Proof

Step Hyp Ref Expression
1 axunndlem1 
 |-  E. w A. y ( E. w ( y e. w /\ w e. z ) -> y e. w )
2 nfnae 
 |-  F/ x -. A. x x = y
3 nfnae 
 |-  F/ x -. A. x x = z
4 2 3 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
5 nfnae 
 |-  F/ y -. A. x x = y
6 nfnae 
 |-  F/ y -. A. x x = z
7 5 6 nfan 
 |-  F/ y ( -. A. x x = y /\ -. A. x x = z )
8 nfv 
 |-  F/ w ( -. A. x x = y /\ -. A. x x = z )
9 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
10 9 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x y )
11 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x w )
12 10 11 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y e. w )
13 nfcvf 
 |-  ( -. A. x x = z -> F/_ x z )
14 13 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ x z )
15 11 14 nfeld 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w e. z )
16 12 15 nfand 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( y e. w /\ w e. z ) )
17 8 16 nfexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. w ( y e. w /\ w e. z ) )
18 17 12 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. w ( y e. w /\ w e. z ) -> y e. w ) )
19 7 18 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y ( E. w ( y e. w /\ w e. z ) -> y e. w ) )
20 nfcvd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y w )
21 nfcvf2 
 |-  ( -. A. x x = y -> F/_ y x )
22 21 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/_ y x )
23 20 22 nfeqd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
24 7 23 nfan1 
 |-  F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
25 elequ2 
 |-  ( w = x -> ( y e. w <-> y e. x ) )
26 elequ1 
 |-  ( w = x -> ( w e. z <-> x e. z ) )
27 25 26 anbi12d 
 |-  ( w = x -> ( ( y e. w /\ w e. z ) <-> ( y e. x /\ x e. z ) ) )
28 27 a1i 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( y e. w /\ w e. z ) <-> ( y e. x /\ x e. z ) ) ) )
29 4 16 28 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w ( y e. w /\ w e. z ) <-> E. x ( y e. x /\ x e. z ) ) )
30 29 adantr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. w ( y e. w /\ w e. z ) <-> E. x ( y e. x /\ x e. z ) ) )
31 25 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( y e. w <-> y e. x ) )
32 30 31 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. w ( y e. w /\ w e. z ) -> y e. w ) <-> ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
33 24 32 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y ( E. w ( y e. w /\ w e. z ) -> y e. w ) <-> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
34 33 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( A. y ( E. w ( y e. w /\ w e. z ) -> y e. w ) <-> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) ) )
35 4 19 34 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w A. y ( E. w ( y e. w /\ w e. z ) -> y e. w ) <-> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
36 1 35 mpbii 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
37 36 ex 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) ) )
38 nfae 
 |-  F/ y A. x x = y
39 nfae 
 |-  F/ x A. x x = y
40 elirrv 
 |-  -. y e. y
41 elequ2 
 |-  ( x = y -> ( y e. x <-> y e. y ) )
42 40 41 mtbiri 
 |-  ( x = y -> -. y e. x )
43 42 intnanrd 
 |-  ( x = y -> -. ( y e. x /\ x e. z ) )
44 43 sps 
 |-  ( A. x x = y -> -. ( y e. x /\ x e. z ) )
45 39 44 nexd 
 |-  ( A. x x = y -> -. E. x ( y e. x /\ x e. z ) )
46 45 pm2.21d 
 |-  ( A. x x = y -> ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
47 38 46 alrimi 
 |-  ( A. x x = y -> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
48 47 19.8ad 
 |-  ( A. x x = y -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
49 nfae 
 |-  F/ y A. x x = z
50 nfae 
 |-  F/ x A. x x = z
51 elirrv 
 |-  -. z e. z
52 elequ1 
 |-  ( x = z -> ( x e. z <-> z e. z ) )
53 51 52 mtbiri 
 |-  ( x = z -> -. x e. z )
54 53 intnand 
 |-  ( x = z -> -. ( y e. x /\ x e. z ) )
55 54 sps 
 |-  ( A. x x = z -> -. ( y e. x /\ x e. z ) )
56 50 55 nexd 
 |-  ( A. x x = z -> -. E. x ( y e. x /\ x e. z ) )
57 56 pm2.21d 
 |-  ( A. x x = z -> ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
58 49 57 alrimi 
 |-  ( A. x x = z -> A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
59 58 19.8ad 
 |-  ( A. x x = z -> E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) )
60 37 48 59 pm2.61ii 
 |-  E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )