Metamath Proof Explorer

Theorem axunndlem1

Description: Lemma for 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 axunndlem1 ⊢∃x∀y∃xy∈x∧x∈z→y∈x

Proof

Step Hyp Ref Expression
1 en2lp ⊢¬y∈x∧x∈y
2 elequ2 ⊢y=z→x∈y↔x∈z
3 2 anbi2d ⊢y=z→y∈x∧x∈y↔y∈x∧x∈z
4 1 3 mtbii ⊢y=z→¬y∈x∧x∈z
5 4 sps ⊢∀yy=z→¬y∈x∧x∈z
6 5 nexdv ⊢∀yy=z→¬∃xy∈x∧x∈z
7 6 pm2.21d ⊢∀yy=z→∃xy∈x∧x∈z→y∈x
8 7 axc4i ⊢∀yy=z→∀y∃xy∈x∧x∈z→y∈x
9 8 19.8ad ⊢∀yy=z→∃x∀y∃xy∈x∧x∈z→y∈x
10 zfun ⊢∃x∀w∃xw∈x∧x∈z→w∈x
11 nfnae ⊢Ⅎy¬∀yy=z
12 nfnae ⊢Ⅎx¬∀yy=z
13 nfvd ⊢¬∀yy=z→Ⅎyw∈x
14 nfcvf ⊢¬∀yy=z→Ⅎ_yz
15 14 nfcrd ⊢¬∀yy=z→Ⅎyx∈z
16 13 15 nfand ⊢¬∀yy=z→Ⅎyw∈x∧x∈z
17 12 16 nfexd ⊢¬∀yy=z→Ⅎy∃xw∈x∧x∈z
18 17 13 nfimd ⊢¬∀yy=z→Ⅎy∃xw∈x∧x∈z→w∈x
19 elequ1 ⊢w=y→w∈x↔y∈x
20 19 anbi1d ⊢w=y→w∈x∧x∈z↔y∈x∧x∈z
21 20 exbidv ⊢w=y→∃xw∈x∧x∈z↔∃xy∈x∧x∈z
22 21 19 imbi12d ⊢w=y→∃xw∈x∧x∈z→w∈x↔∃xy∈x∧x∈z→y∈x
23 22 a1i ⊢¬∀yy=z→w=y→∃xw∈x∧x∈z→w∈x↔∃xy∈x∧x∈z→y∈x
24 11 18 23 cbvald ⊢¬∀yy=z→∀w∃xw∈x∧x∈z→w∈x↔∀y∃xy∈x∧x∈z→y∈x
25 24 exbidv ⊢¬∀yy=z→∃x∀w∃xw∈x∧x∈z→w∈x↔∃x∀y∃xy∈x∧x∈z→y∈x
26 10 25 mpbii ⊢¬∀yy=z→∃x∀y∃xy∈x∧x∈z→y∈x
27 9 26 pm2.61i ⊢∃x∀y∃xy∈x∧x∈z→y∈x