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 )