Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac4 Unicode version

Theorem dfac4 7950
 Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of [BellMachover] p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
dfac4 CHOICE
Distinct variable group:   ,,

Proof of Theorem dfac4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 7949 . 2 CHOICE
2 fveq1 5681 . . . . . . . . 9
32eleq1d 2467 . . . . . . . 8
43imbi2d 308 . . . . . . 7
54ralbidv 2683 . . . . . 6
65cbvexv 2051 . . . . 5
7 fvex 5696 . . . . . . . . 9
8 eqid 2401 . . . . . . . . 9
97, 8fnmpti 5527 . . . . . . . 8
10 fveq2 5682 . . . . . . . . . . . . 13
11 fvex 5696 . . . . . . . . . . . . 13
1210, 8, 11fvmpt 5759 . . . . . . . . . . . 12
1312eleq1d 2467 . . . . . . . . . . 11
1413imbi2d 308 . . . . . . . . . 10
1514ralbiia 2695 . . . . . . . . 9
1615anbi2i 676 . . . . . . . 8
179, 16mpbiran 885 . . . . . . 7
18 fvrn0 5707 . . . . . . . . . . 11
1918rgenw 2730 . . . . . . . . . 10
208fmpt 5843 . . . . . . . . . 10
2119, 20mpbi 200 . . . . . . . . 9
22 vex 2916 . . . . . . . . 9
23 vex 2916 . . . . . . . . . . 11
2423rnex 5087 . . . . . . . . . 10
25 p0ex 4341 . . . . . . . . . 10
2624, 25unex 4661 . . . . . . . . 9
27 fex2 5557 . . . . . . . . 9
2821, 22, 26, 27mp3an 1279 . . . . . . . 8
29 fneq1 5488 . . . . . . . . 9
30 fveq1 5681 . . . . . . . . . . . 12
3130eleq1d 2467 . . . . . . . . . . 11
3231imbi2d 308 . . . . . . . . . 10
3332ralbidv 2683 . . . . . . . . 9
3429, 33anbi12d 692 . . . . . . . 8
3528, 34spcev 3000 . . . . . . 7
3617, 35sylbir 205 . . . . . 6
3736exlimiv 1641 . . . . 5
386, 37sylbi 188 . . . 4
39 simpr 448 . . . . 5
4039eximi 1582 . . . 4
4138, 40impbii 181 . . 3
4241albii 1572 . 2
431, 42bitri 241 1 CHOICE
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1546  wex 1547   wceq 1649   wcel 1721   wne 2564  wral 2663  cvv 2913   cun 3275  c0 3585  csn 3771   cmpt 4221   crn 4833   wfn 5403  wf 5404  cfv 5408  CHOICEwac 7943 This theorem is referenced by:  dfac5  7956  dfacacn  7968  ac5  8304 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-sbc 3119  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-br 4168  df-opab 4222  df-mpt 4223  df-id 4453  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-fv 5416  df-ac 7944
 Copyright terms: Public domain W3C validator