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

Theorem dfiun2g 3935
 Description: Alternate definition of indexed union when is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
dfiun2g
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   (,)

Proof of Theorem dfiun2g
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfra1 2593 . . . . . 6
2 rsp 2603 . . . . . . . 8
3 clel3g 2905 . . . . . . . 8
42, 3syl6 29 . . . . . . 7
54imp 418 . . . . . 6
61, 5rexbida 2558 . . . . 5
7 rexcom4 2807 . . . . 5
86, 7syl6bb 252 . . . 4
9 r19.41v 2693 . . . . . 6
109exbii 1569 . . . . 5
11 exancom 1573 . . . . 5
1210, 11bitri 240 . . . 4
138, 12syl6bb 252 . . 3
14 eliun 3909 . . 3
15 eluniab 3839 . . 3
1613, 14, 153bitr4g 279 . 2
1716eqrdv 2281 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wex 1528   wceq 1623   wcel 1684  cab 2269  wral 2543  wrex 2544  cuni 3827  ciun 3905 This theorem is referenced by:  dfiun2  3937  dfiun3g  4931  iunexg  5767  uniqs  6719  ac6num  8106  iunopn  16644  pnrmopn  17071  cncmp  17119  ptcmplem3  17748  iunmbl  18910  voliun  18911  sigaclcuni  23479  sigaclcu2  23481  sigaclci  23493  measvunilem  23540  meascnbl  23546 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-uni 3828  df-iun 3907
 Copyright terms: Public domain W3C validator