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

Theorem dfiun2 3911
 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:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem dfiun2
StepHypRef Expression
1 dfiun2g 3909 . 2
2 dfiun2.1 . . 3
32a1i 12 . 2
41, 3mprg 2587 1
 Colors of variables: wff set class Syntax hints:   wceq 1619   wcel 1621  cab 2244  wrex 2519  cvv 2763  cuni 3801  ciun 3879 This theorem is referenced by:  funcnvuni  5255  fun11iun  5431  fniunfv  5707  tfrlem8  6368  rdglim2a  6414  rankuni  7503  cardiun  7583  kmlem11  7754  cfslb2n  7862  enfin2i  7915  pwcfsdom  8173  rankcf  8367  tskuni  8373  discmp  17087  cmpsublem  17088  cmpsub  17089 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ral 2523  df-rex 2524  df-v 2765  df-uni 3802  df-iun 3881
 Copyright terms: Public domain W3C validator