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

Theorem dfiun2 4364
 Description: Alternate definition of indexed union when is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
Hypothesis
Ref Expression
dfiun2.1
Assertion
Ref Expression
dfiun2
Distinct variable groups:   ,   ,   ,

Proof of Theorem dfiun2
StepHypRef Expression
1 dfiun2g 4362 . 2
2 dfiun2.1 . . 3
32a1i 11 . 2
41, 3mprg 2820 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  e.wcel 1818  {cab 2442  E.wrex 2808   cvv 3109  U.cuni 4249  U_ciun 4330 This theorem is referenced by:  fniunfv  6159  funcnvuni  6753  fun11iun  6760  tfrlem8  7072  rdglim2a  7118  rankuni  8302  cardiun  8384  kmlem11  8561  cfslb2n  8669  enfin2i  8722  pwcfsdom  8979  rankcf  9176  tskuni  9182  discmp  19898  cmpsublem  19899  cmpsub  19900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-uni 4250  df-iun 4332
 Copyright terms: Public domain W3C validator