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

Theorem dfco2a 5334
 Description: Generalization of dfco2 5333, where can have any value between and . (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
dfco2a
Distinct variable groups:   ,   ,   ,

Proof of Theorem dfco2a
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfco2 5333 . 2
2 vex 3047 . . . . . . . . . . . . . 14
3 vex 3047 . . . . . . . . . . . . . . 15
43eliniseg 5196 . . . . . . . . . . . . . 14
52, 4ax-mp 5 . . . . . . . . . . . . 13
63, 2brelrn 5064 . . . . . . . . . . . . 13
75, 6sylbi 199 . . . . . . . . . . . 12
8 vex 3047 . . . . . . . . . . . . . 14
92, 8elimasn 5192 . . . . . . . . . . . . 13
102, 8opeldm 5037 . . . . . . . . . . . . 13
119, 10sylbi 199 . . . . . . . . . . . 12
127, 11anim12ci 570 . . . . . . . . . . 11
1312adantl 468 . . . . . . . . . 10
1413exlimivv 1777 . . . . . . . . 9
15 elxp 4850 . . . . . . . . 9
16 elin 3616 . . . . . . . . 9
1714, 15, 163imtr4i 270 . . . . . . . 8
18 ssel 3425 . . . . . . . 8
1917, 18syl5 33 . . . . . . 7
2019pm4.71rd 640 . . . . . 6
2120exbidv 1767 . . . . 5
22 rexv 3061 . . . . 5
23 df-rex 2742 . . . . 5
2421, 22, 233bitr4g 292 . . . 4
25 eliun 4282 . . . 4
26 eliun 4282 . . . 4
2724, 25, 263bitr4g 292 . . 3
2827eqrdv 2448 . 2
291, 28syl5eq 2496 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443  wex 1662   wcel 1886  wrex 2737  cvv 3044   cin 3402   wss 3403  csn 3967  cop 3973  ciun 4277   class class class wbr 4401   cxp 4831  ccnv 4832   cdm 4833   crn 4834  cima 4836   ccom 4837 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-iun 4279  df-br 4402  df-opab 4461  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846 This theorem is referenced by:  fparlem3  6895  fparlem4  6896
 Copyright terms: Public domain W3C validator