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 𝑥𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 )

Proof

Step Hyp Ref Expression
1 en2lp ¬ ( 𝑦𝑥𝑥𝑦 )
2 elequ2 ( 𝑦 = 𝑧 → ( 𝑥𝑦𝑥𝑧 ) )
3 2 anbi2d ( 𝑦 = 𝑧 → ( ( 𝑦𝑥𝑥𝑦 ) ↔ ( 𝑦𝑥𝑥𝑧 ) ) )
4 1 3 mtbii ( 𝑦 = 𝑧 → ¬ ( 𝑦𝑥𝑥𝑧 ) )
5 4 sps ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ( 𝑦𝑥𝑥𝑧 ) )
6 5 nexdv ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) )
7 6 pm2.21d ( ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) )
8 7 axc4i ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) )
9 8 19.8ad ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) )
10 zfun 𝑥𝑤 ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 )
11 nfnae 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
12 nfnae 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
13 nfvd ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑤𝑥 )
14 nfcvf ( ¬ ∀ 𝑦 𝑦 = 𝑧 𝑦 𝑧 )
15 14 nfcrd ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑥𝑧 )
16 13 15 nfand ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( 𝑤𝑥𝑥𝑧 ) )
17 12 16 nfexd ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦𝑥 ( 𝑤𝑥𝑥𝑧 ) )
18 17 13 nfimd ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 ) )
19 elequ1 ( 𝑤 = 𝑦 → ( 𝑤𝑥𝑦𝑥 ) )
20 19 anbi1d ( 𝑤 = 𝑦 → ( ( 𝑤𝑥𝑥𝑧 ) ↔ ( 𝑦𝑥𝑥𝑧 ) ) )
21 20 exbidv ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) ↔ ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) ) )
22 21 19 imbi12d ( 𝑤 = 𝑦 → ( ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 ) ↔ ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) ) )
23 22 a1i ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑦 → ( ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 ) ↔ ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) ) ) )
24 11 18 23 cbvald ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑤 ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) ) )
25 24 exbidv ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑥𝑤 ( ∃ 𝑥 ( 𝑤𝑥𝑥𝑧 ) → 𝑤𝑥 ) ↔ ∃ 𝑥𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) ) )
26 10 25 mpbii ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 ) )
27 9 26 pm2.61i 𝑥𝑦 ( ∃ 𝑥 ( 𝑦𝑥𝑥𝑧 ) → 𝑦𝑥 )