Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  indexa Structured version   Unicode version

Theorem indexa 29678
 Description: If for every element of an indexing set there exists a corresponding element of another set , then there exists a subset of consisting only of those elements which are indexed by . Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
indexa
Distinct variable groups:   ,,,   ,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem indexa
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rabexg 4590 . 2
2 ssrab2 3578 . . . 4
32a1i 11 . . 3
4 nfv 1678 . . . . 5
5 nfre1 2918 . . . . 5
6 sbceq2a 3336 . . . . . . . . . . . . . . 15
76rspcev 3207 . . . . . . . . . . . . . 14
87ancoms 453 . . . . . . . . . . . . 13
98anim2i 569 . . . . . . . . . . . 12
109ancoms 453 . . . . . . . . . . 11
1110anasss 647 . . . . . . . . . 10
1211ancoms 453 . . . . . . . . 9
13 sbceq2a 3336 . . . . . . . . . . . 12
1413sbcbidv 3383 . . . . . . . . . . 11
1514rexbidv 2966 . . . . . . . . . 10
1615elrab 3254 . . . . . . . . 9
1712, 16sylibr 212 . . . . . . . 8
18 sbceq2a 3336 . . . . . . . . 9
1918rspcev 3207 . . . . . . . 8
2017, 19sylancom 667 . . . . . . 7
21 nfcv 2622 . . . . . . . 8
22 nfcv 2622 . . . . . . . . . 10
23 nfcv 2622 . . . . . . . . . . 11
24 nfsbc1v 3344 . . . . . . . . . . 11
2523, 24nfsbc 3346 . . . . . . . . . 10
2622, 25nfrex 2920 . . . . . . . . 9
27 nfcv 2622 . . . . . . . . 9
2826, 27nfrab 3036 . . . . . . . 8
29 nfsbc1v 3344 . . . . . . . 8
30 nfv 1678 . . . . . . . 8
3121, 28, 29, 30, 18cbvrexf 3076 . . . . . . 7
3220, 31sylib 196 . . . . . 6
3332exp31 604 . . . . 5
344, 5, 33rexlimd 2940 . . . 4
3534ralimia 2848 . . 3
36 nfsbc1v 3344 . . . . . . . . 9
37 nfv 1678 . . . . . . . . 9
3836, 37, 6cbvrex 3078 . . . . . . . 8
3915, 38syl6bb 261 . . . . . . 7
4039elrab 3254 . . . . . 6
4140simprbi 464 . . . . 5
4241rgen 2817 . . . 4
4342a1i 11 . . 3
443, 35, 433jca 1171 . 2
45 sseq1 3518 . . . . 5
46 nfcv 2622 . . . . . . . . 9
47 nfsbc1v 3344 . . . . . . . . 9
4846, 47nfrex 2920 . . . . . . . 8
49 nfcv 2622 . . . . . . . 8
5048, 49nfrab 3036 . . . . . . 7
5150nfeq2 2639 . . . . . 6
52 nfcv 2622 . . . . . . 7
5352, 28rexeqf 3048 . . . . . 6
5451, 53ralbid 2891 . . . . 5
5552, 28raleqf 3047 . . . . 5
5645, 54, 553anbi123d 1294 . . . 4
5756spcegv 3192 . . 3
5857imp 429 . 2
591, 44, 58syl2an 477 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 968   wceq 1374  wex 1591   wcel 1762  wral 2807  wrex 2808  crab 2811  cvv 3106  wsbc 3324   wss 3469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-in 3476  df-ss 3483 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator