MPE Home 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  B 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  |-  B  e. 
_V
Assertion
Ref Expression
dfiun2  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Distinct variable groups:    x, y    y, A    y, B
Allowed substitution hints:    A( x)    B( x)

Proof of Theorem dfiun2
StepHypRef Expression
1 dfiun2g 3909 . 2  |-  ( A. x  e.  A  B  e.  _V  ->  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B } )
2 dfiun2.1 . . 3  |-  B  e. 
_V
32a1i 12 . 2  |-  ( x  e.  A  ->  B  e.  _V )
41, 3mprg 2587 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   {cab 2244   E.wrex 2519   _Vcvv 2763   U.cuni 3801   U_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