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

Theorem dfiun2 4330
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 4328 . 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 2788 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1868   {cab 2407   E.wrex 2776   _Vcvv 3081   U.cuni 4216   U_ciun 4296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-v 3083  df-uni 4217  df-iun 4298
This theorem is referenced by:  fniunfv  6163  funcnvuni  6756  fun11iun  6763  tfrlem8  7106  rdglim2a  7155  rankuni  8335  cardiun  8417  kmlem11  8590  cfslb2n  8698  enfin2i  8751  pwcfsdom  9008  rankcf  9202  tskuni  9208  discmp  20397  cmpsublem  20398  cmpsub  20399
  Copyright terms: Public domain W3C validator