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

Theorem dfac3 7986
 Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is the Axiom of Choice of [TakeutiZaring] p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
dfac3 CHOICE
Distinct variable group:   ,,

Proof of Theorem dfac3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ac 7981 . 2 CHOICE
2 vex 2946 . . . . . . . 8
32uniex 4691 . . . . . . . 8
42, 3xpex 4976 . . . . . . 7
5 simpl 444 . . . . . . . . . 10
6 elunii 4007 . . . . . . . . . . 11
76ancoms 440 . . . . . . . . . 10
85, 7jca 519 . . . . . . . . 9
98ssopab2i 4469 . . . . . . . 8
10 df-xp 4870 . . . . . . . 8
119, 10sseqtr4i 3368 . . . . . . 7
124, 11ssexi 4335 . . . . . 6
13 sseq2 3357 . . . . . . . 8
14 dmeq 5056 . . . . . . . . 9
1514fneq2d 5523 . . . . . . . 8
1613, 15anbi12d 692 . . . . . . 7
1716exbidv 1636 . . . . . 6
1812, 17spcv 3029 . . . . 5
19 fndm 5530 . . . . . . . . . . . . 13
20 eleq2 2491 . . . . . . . . . . . . . 14
21 dmopab 5066 . . . . . . . . . . . . . . . 16
2221eleq2i 2494 . . . . . . . . . . . . . . 15
23 vex 2946 . . . . . . . . . . . . . . . 16
24 elequ1 1728 . . . . . . . . . . . . . . . . . 18
25 eleq2 2491 . . . . . . . . . . . . . . . . . 18
2624, 25anbi12d 692 . . . . . . . . . . . . . . . . 17
2726exbidv 1636 . . . . . . . . . . . . . . . 16
2823, 27elab 3069 . . . . . . . . . . . . . . 15
29 19.42v 1928 . . . . . . . . . . . . . . . 16
30 n0 3624 . . . . . . . . . . . . . . . . 17
3130anbi2i 676 . . . . . . . . . . . . . . . 16
3229, 31bitr4i 244 . . . . . . . . . . . . . . 15
3322, 28, 323bitrri 264 . . . . . . . . . . . . . 14
3420, 33syl6rbbr 256 . . . . . . . . . . . . 13
3519, 34syl 16 . . . . . . . . . . . 12
3635adantl 453 . . . . . . . . . . 11
37 fnfun 5528 . . . . . . . . . . . 12
38 funfvima3 5961 . . . . . . . . . . . . 13
3938ancoms 440 . . . . . . . . . . . 12
4037, 39sylan2 461 . . . . . . . . . . 11
4136, 40sylbid 207 . . . . . . . . . 10
4241imp 419 . . . . . . . . 9
43 ibar 491 . . . . . . . . . . . . 13
4443abbi2dv 2545 . . . . . . . . . . . 12
45 imasng 5212 . . . . . . . . . . . . . 14
4623, 45ax-mp 8 . . . . . . . . . . . . 13
47 vex 2946 . . . . . . . . . . . . . . 15
48 elequ1 1728 . . . . . . . . . . . . . . . 16
4948anbi2d 685 . . . . . . . . . . . . . . 15
50 eqid 2430 . . . . . . . . . . . . . . 15
5123, 47, 26, 49, 50brab 4464 . . . . . . . . . . . . . 14
5251abbii 2542 . . . . . . . . . . . . 13
5346, 52eqtri 2450 . . . . . . . . . . . 12
5444, 53syl6reqr 2481 . . . . . . . . . . 11
5554eleq2d 2497 . . . . . . . . . 10
5655ad2antrl 709 . . . . . . . . 9
5742, 56mpbid 202 . . . . . . . 8
5857exp32 589 . . . . . . 7
5958ralrimiv 2775 . . . . . 6
6059eximi 1585 . . . . 5
6118, 60syl 16 . . . 4
6261alrimiv 1641 . . 3
63 eqid 2430 . . . . 5
6463aceq3lem 7985 . . . 4
6564alrimiv 1641 . . 3
6662, 65impbii 181 . 2
671, 66bitri 241 1 CHOICE
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1549  wex 1550   wceq 1652   wcel 1725  cab 2416   wne 2593  wral 2692  cvv 2943   wss 3307  c0 3615  csn 3801  cuni 4002   class class class wbr 4199  copab 4252   cmpt 4253   cxp 4862   cdm 4864  cima 4867   wfun 5434   wfn 5435  cfv 5440  CHOICEwac 7980 This theorem is referenced by:  dfac4  7987  dfac5  7993  dfac2a  7994  dfac2  7995  dfac8  7999  dfac9  8000  ac4  8339  dfac11  27070 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-mpt 4255  df-id 4485  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-iota 5404  df-fun 5442  df-fn 5443  df-fv 5448  df-ac 7981
 Copyright terms: Public domain W3C validator