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

Theorem dfiun2 4312
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 4310 . 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 2751 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444    e. wcel 1887   {cab 2437   E.wrex 2738   _Vcvv 3045   U.cuni 4198   U_ciun 4278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-v 3047  df-uni 4199  df-iun 4280
This theorem is referenced by:  fniunfv  6152  funcnvuni  6746  fun11iun  6753  tfrlem8  7102  rdglim2a  7151  rankuni  8334  cardiun  8416  kmlem11  8590  cfslb2n  8698  enfin2i  8751  pwcfsdom  9008  rankcf  9202  tskuni  9208  discmp  20413  cmpsublem  20414  cmpsub  20415
  Copyright terms: Public domain W3C validator