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 ⊢∃x∀y∃xy∈x∧x∈z→y∈x

Proof

Step Hyp Ref Expression
1 axunndlem1 ⊢∃w∀y∃wy∈w∧w∈z→y∈w
2 nfnae ⊢Ⅎx¬∀xx=y
3 nfnae ⊢Ⅎx¬∀xx=z
4 2 3 nfan ⊢Ⅎx¬∀xx=y∧¬∀xx=z
5 nfnae ⊢Ⅎy¬∀xx=y
6 nfnae ⊢Ⅎy¬∀xx=z
7 5 6 nfan ⊢Ⅎy¬∀xx=y∧¬∀xx=z
8 nfv ⊢Ⅎw¬∀xx=y∧¬∀xx=z
9 nfcvf ⊢¬∀xx=y→Ⅎ_xy
10 9 adantr ⊢¬∀xx=y∧¬∀xx=z→Ⅎ_xy
11 nfcvd ⊢¬∀xx=y∧¬∀xx=z→Ⅎ_xw
12 10 11 nfeld ⊢¬∀xx=y∧¬∀xx=z→Ⅎxy∈w
13 nfcvf ⊢¬∀xx=z→Ⅎ_xz
14 13 adantl ⊢¬∀xx=y∧¬∀xx=z→Ⅎ_xz
15 11 14 nfeld ⊢¬∀xx=y∧¬∀xx=z→Ⅎxw∈z
16 12 15 nfand ⊢¬∀xx=y∧¬∀xx=z→Ⅎxy∈w∧w∈z
17 8 16 nfexd ⊢¬∀xx=y∧¬∀xx=z→Ⅎx∃wy∈w∧w∈z
18 17 12 nfimd ⊢¬∀xx=y∧¬∀xx=z→Ⅎx∃wy∈w∧w∈z→y∈w
19 7 18 nfald ⊢¬∀xx=y∧¬∀xx=z→Ⅎx∀y∃wy∈w∧w∈z→y∈w
20 nfcvd ⊢¬∀xx=y∧¬∀xx=z→Ⅎ_yw
21 nfcvf2 ⊢¬∀xx=y→Ⅎ_yx
22 21 adantr ⊢¬∀xx=y∧¬∀xx=z→Ⅎ_yx
23 20 22 nfeqd ⊢¬∀xx=y∧¬∀xx=z→Ⅎyw=x
24 7 23 nfan1 ⊢Ⅎy¬∀xx=y∧¬∀xx=z∧w=x
25 elequ2 ⊢w=x→y∈w↔y∈x
26 elequ1 ⊢w=x→w∈z↔x∈z
27 25 26 anbi12d ⊢w=x→y∈w∧w∈z↔y∈x∧x∈z
28 27 a1i ⊢¬∀xx=y∧¬∀xx=z→w=x→y∈w∧w∈z↔y∈x∧x∈z
29 4 16 28 cbvexd ⊢¬∀xx=y∧¬∀xx=z→∃wy∈w∧w∈z↔∃xy∈x∧x∈z
30 29 adantr ⊢¬∀xx=y∧¬∀xx=z∧w=x→∃wy∈w∧w∈z↔∃xy∈x∧x∈z
31 25 adantl ⊢¬∀xx=y∧¬∀xx=z∧w=x→y∈w↔y∈x
32 30 31 imbi12d ⊢¬∀xx=y∧¬∀xx=z∧w=x→∃wy∈w∧w∈z→y∈w↔∃xy∈x∧x∈z→y∈x
33 24 32 albid ⊢¬∀xx=y∧¬∀xx=z∧w=x→∀y∃wy∈w∧w∈z→y∈w↔∀y∃xy∈x∧x∈z→y∈x
34 33 ex ⊢¬∀xx=y∧¬∀xx=z→w=x→∀y∃wy∈w∧w∈z→y∈w↔∀y∃xy∈x∧x∈z→y∈x
35 4 19 34 cbvexd ⊢¬∀xx=y∧¬∀xx=z→∃w∀y∃wy∈w∧w∈z→y∈w↔∃x∀y∃xy∈x∧x∈z→y∈x
36 1 35 mpbii ⊢¬∀xx=y∧¬∀xx=z→∃x∀y∃xy∈x∧x∈z→y∈x
37 36 ex ⊢¬∀xx=y→¬∀xx=z→∃x∀y∃xy∈x∧x∈z→y∈x
38 nfae ⊢Ⅎy∀xx=y
39 nfae ⊢Ⅎx∀xx=y
40 elirrv ⊢¬y∈y
41 elequ2 ⊢x=y→y∈x↔y∈y
42 40 41 mtbiri ⊢x=y→¬y∈x
43 42 intnanrd ⊢x=y→¬y∈x∧x∈z
44 43 sps ⊢∀xx=y→¬y∈x∧x∈z
45 39 44 nexd ⊢∀xx=y→¬∃xy∈x∧x∈z
46 45 pm2.21d ⊢∀xx=y→∃xy∈x∧x∈z→y∈x
47 38 46 alrimi ⊢∀xx=y→∀y∃xy∈x∧x∈z→y∈x
48 47 19.8ad ⊢∀xx=y→∃x∀y∃xy∈x∧x∈z→y∈x
49 nfae ⊢Ⅎy∀xx=z
50 nfae ⊢Ⅎx∀xx=z
51 elirrv ⊢¬z∈z
52 elequ1 ⊢x=z→x∈z↔z∈z
53 51 52 mtbiri ⊢x=z→¬x∈z
54 53 intnand ⊢x=z→¬y∈x∧x∈z
55 54 sps ⊢∀xx=z→¬y∈x∧x∈z
56 50 55 nexd ⊢∀xx=z→¬∃xy∈x∧x∈z
57 56 pm2.21d ⊢∀xx=z→∃xy∈x∧x∈z→y∈x
58 49 57 alrimi ⊢∀xx=z→∀y∃xy∈x∧x∈z→y∈x
59 58 19.8ad ⊢∀xx=z→∃x∀y∃xy∈x∧x∈z→y∈x
60 37 48 59 pm2.61ii ⊢∃x∀y∃xy∈x∧x∈z→y∈x