MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axunndlem1 Structured version   Visualization version   GIF version

Theorem axunndlem1 10635
Description: Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
Assertion
Ref Expression
axunndlem1 𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)
Distinct variable groups:   𝑥,𝑦   𝑥,𝑧

Proof of Theorem axunndlem1
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 en2lp 9646 . . . . . . . 8 ¬ (𝑦𝑥𝑥𝑦)
2 elequ2 2123 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑥𝑦𝑥𝑧))
32anbi2d 630 . . . . . . . 8 (𝑦 = 𝑧 → ((𝑦𝑥𝑥𝑦) ↔ (𝑦𝑥𝑥𝑧)))
41, 3mtbii 326 . . . . . . 7 (𝑦 = 𝑧 → ¬ (𝑦𝑥𝑥𝑧))
54sps 2185 . . . . . 6 (∀𝑦 𝑦 = 𝑧 → ¬ (𝑦𝑥𝑥𝑧))
65nexdv 1936 . . . . 5 (∀𝑦 𝑦 = 𝑧 → ¬ ∃𝑥(𝑦𝑥𝑥𝑧))
76pm2.21d 121 . . . 4 (∀𝑦 𝑦 = 𝑧 → (∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥))
87axc4i 2322 . . 3 (∀𝑦 𝑦 = 𝑧 → ∀𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥))
9819.8ad 2182 . 2 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥))
10 zfun 7756 . . 3 𝑥𝑤(∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥)
11 nfnae 2439 . . . . 5 𝑦 ¬ ∀𝑦 𝑦 = 𝑧
12 nfnae 2439 . . . . . . 7 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
13 nfvd 1915 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤𝑥)
14 nfcvf 2932 . . . . . . . . 9 (¬ ∀𝑦 𝑦 = 𝑧𝑦𝑧)
1514nfcrd 2899 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥𝑧)
1613, 15nfand 1897 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑤𝑥𝑥𝑧))
1712, 16nfexd 2329 . . . . . 6 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑥(𝑤𝑥𝑥𝑧))
1817, 13nfimd 1894 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥))
19 elequ1 2115 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤𝑥𝑦𝑥))
2019anbi1d 631 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑤𝑥𝑥𝑧) ↔ (𝑦𝑥𝑥𝑧)))
2120exbidv 1921 . . . . . . 7 (𝑤 = 𝑦 → (∃𝑥(𝑤𝑥𝑥𝑧) ↔ ∃𝑥(𝑦𝑥𝑥𝑧)))
2221, 19imbi12d 344 . . . . . 6 (𝑤 = 𝑦 → ((∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥) ↔ (∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)))
2322a1i 11 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → ((∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥) ↔ (∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥))))
2411, 18, 23cbvald 2412 . . . 4 (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑤(∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥) ↔ ∀𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)))
2524exbidv 1921 . . 3 (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑥𝑤(∃𝑥(𝑤𝑥𝑥𝑧) → 𝑤𝑥) ↔ ∃𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)))
2610, 25mpbii 233 . 2 (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥))
279, 26pm2.61i 182 1 𝑥𝑦(∃𝑥(𝑦𝑥𝑥𝑧) → 𝑦𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-reg 9632
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-eprel 5584  df-fr 5637
This theorem is referenced by:  axunnd  10636
  Copyright terms: Public domain W3C validator