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

Theorem dfiun2 4345
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 4343 . 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 2804 1  |-  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    e. wcel 1802   {cab 2426   E.wrex 2792   _Vcvv 3093   U.cuni 4230   U_ciun 4311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-v 3095  df-uni 4231  df-iun 4313
This theorem is referenced by:  fniunfv  6140  funcnvuni  6734  fun11iun  6741  tfrlem8  7051  rdglim2a  7097  rankuni  8279  cardiun  8361  kmlem11  8538  cfslb2n  8646  enfin2i  8699  pwcfsdom  8956  rankcf  9153  tskuni  9159  discmp  19764  cmpsublem  19765  cmpsub  19766
  Copyright terms: Public domain W3C validator