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

Theorem dfiun2 4112
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 4110 . 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 2762 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   {cab 2416   E.wrex 2693   _Vcvv 2943   U.cuni 4002   U_ciun 4080
This theorem is referenced by:  funcnvuni  5504  fun11iun  5681  fniunfv  5980  tfrlem8  6631  rdglim2a  6677  rankuni  7773  cardiun  7853  kmlem11  8024  cfslb2n  8132  enfin2i  8185  pwcfsdom  8442  rankcf  8636  tskuni  8642  discmp  17444  cmpsublem  17445  cmpsub  17446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ral 2697  df-rex 2698  df-v 2945  df-uni 4003  df-iun 4082
  Copyright terms: Public domain W3C validator