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

Theorem aceq2 9579
 Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004.)
Assertion
Ref Expression
aceq2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢

Proof of Theorem aceq2
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 df-ral 3075 . . . . 5 (∀𝑡𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑡(𝑡𝑧 → ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2 19.23v 1943 . . . . 5 (∀𝑡(𝑡𝑧 → ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)) ↔ (∃𝑡 𝑡𝑧 → ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
31, 2bitri 278 . . . 4 (∀𝑡𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ (∃𝑡 𝑡𝑧 → ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
4 biidd 265 . . . . 5 (𝑤 = 𝑡 → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
54cbvralvw 3361 . . . 4 (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑡𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢))
6 n0 4245 . . . . 5 (𝑧 ≠ ∅ ↔ ∃𝑡 𝑡𝑧)
7 elequ2 2126 . . . . . . . . 9 (𝑣 = 𝑢 → (𝑧𝑣𝑧𝑢))
8 elequ2 2126 . . . . . . . . 9 (𝑣 = 𝑢 → (𝑤𝑣𝑤𝑢))
97, 8anbi12d 633 . . . . . . . 8 (𝑣 = 𝑢 → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑢𝑤𝑢)))
109cbvrexvw 3362 . . . . . . 7 (∃𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃𝑢𝑦 (𝑧𝑢𝑤𝑢))
1110reubii 3309 . . . . . 6 (∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃!𝑤𝑧𝑢𝑦 (𝑧𝑢𝑤𝑢))
12 elequ1 2118 . . . . . . . . 9 (𝑤 = 𝑣 → (𝑤𝑢𝑣𝑢))
1312anbi2d 631 . . . . . . . 8 (𝑤 = 𝑣 → ((𝑧𝑢𝑤𝑢) ↔ (𝑧𝑢𝑣𝑢)))
1413rexbidv 3221 . . . . . . 7 (𝑤 = 𝑣 → (∃𝑢𝑦 (𝑧𝑢𝑤𝑢) ↔ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢)))
1514cbvreuvw 3363 . . . . . 6 (∃!𝑤𝑧𝑢𝑦 (𝑧𝑢𝑤𝑢) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢))
1611, 15bitri 278 . . . . 5 (∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢))
176, 16imbi12i 354 . . . 4 ((𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)) ↔ (∃𝑡 𝑡𝑧 → ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
183, 5, 173bitr4i 306 . . 3 (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
1918ralbii 3097 . 2 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
2019exbii 1849 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑤𝑧𝑣𝑦 (𝑧𝑣𝑤𝑣)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  ∃!wreu 3072  ∅c0 4225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-dif 3861  df-nul 4226 This theorem is referenced by:  dfac7  9592  ac3  9922
 Copyright terms: Public domain W3C validator