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

Theorem dfiun2g 4364
 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 2838 . . . . . 6
2 rsp 2823 . . . . . . . 8
3 clel3g 3237 . . . . . . . 8
42, 3syl6 33 . . . . . . 7
54imp 429 . . . . . 6
61, 5rexbida 2963 . . . . 5
7 rexcom4 3129 . . . . 5
86, 7syl6bb 261 . . . 4
9 r19.41v 3009 . . . . . 6
109exbii 1668 . . . . 5
11 exancom 1672 . . . . 5
1210, 11bitri 249 . . . 4
138, 12syl6bb 261 . . 3
14 eliun 4337 . . 3
15 eluniab 4262 . . 3
1613, 14, 153bitr4g 288 . 2
1716eqrdv 2454 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1395  wex 1613   wcel 1819  cab 2442  wral 2807  wrex 2808  cuni 4251  ciun 4332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-uni 4252  df-iun 4334 This theorem is referenced by:  dfiun2  4366  dfiun3g  5265  iunexg  6775  uniqs  7389  ac6num  8876  iunopn  19534  pnrmopn  19971  cncmp  20019  ptcmplem3  20680  iunmbl  22089  voliun  22090  sigaclcuni  28291  sigaclcu2  28293  sigaclci  28305  measvunilem  28356  meascnbl  28363  carsgclctunlem3  28462
 Copyright terms: Public domain W3C validator