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

Theorem dfiun2 4305
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 4303 . 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 11 . 2  |-  ( x  e.  A  ->  B  e.  _V )
41, 3mprg 2896 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   {cab 2436   E.wrex 2796   _Vcvv 3071   U.cuni 4192   U_ciun 4272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-v 3073  df-uni 4193  df-iun 4274
This theorem is referenced by:  fniunfv  6066  funcnvuni  6633  fun11iun  6640  tfrlem8  6946  rdglim2a  6992  rankuni  8174  cardiun  8256  kmlem11  8433  cfslb2n  8541  enfin2i  8594  pwcfsdom  8851  rankcf  9048  tskuni  9054  discmp  19126  cmpsublem  19127  cmpsub  19128
  Copyright terms: Public domain W3C validator