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

Theorem dfiun2g 3951
Description: Alternate definition of indexed union when  B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
dfiun2g  |-  ( A. x  e.  A  B  e.  C  ->  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B } )
Distinct variable groups:    y, A    y, B    x, y
Allowed substitution hints:    A( x)    B( x)    C( x, y)

Proof of Theorem dfiun2g
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfra1 2606 . . . . . 6  |-  F/ x A. x  e.  A  B  e.  C
2 rsp 2616 . . . . . . . 8  |-  ( A. x  e.  A  B  e.  C  ->  ( x  e.  A  ->  B  e.  C ) )
3 clel3g 2918 . . . . . . . 8  |-  ( B  e.  C  ->  (
z  e.  B  <->  E. y
( y  =  B  /\  z  e.  y ) ) )
42, 3syl6 29 . . . . . . 7  |-  ( A. x  e.  A  B  e.  C  ->  ( x  e.  A  ->  (
z  e.  B  <->  E. y
( y  =  B  /\  z  e.  y ) ) ) )
54imp 418 . . . . . 6  |-  ( ( A. x  e.  A  B  e.  C  /\  x  e.  A )  ->  ( z  e.  B  <->  E. y ( y  =  B  /\  z  e.  y ) ) )
61, 5rexbida 2571 . . . . 5  |-  ( A. x  e.  A  B  e.  C  ->  ( E. x  e.  A  z  e.  B  <->  E. x  e.  A  E. y
( y  =  B  /\  z  e.  y ) ) )
7 rexcom4 2820 . . . . 5  |-  ( E. x  e.  A  E. y ( y  =  B  /\  z  e.  y )  <->  E. y E. x  e.  A  ( y  =  B  /\  z  e.  y ) )
86, 7syl6bb 252 . . . 4  |-  ( A. x  e.  A  B  e.  C  ->  ( E. x  e.  A  z  e.  B  <->  E. y E. x  e.  A  ( y  =  B  /\  z  e.  y ) ) )
9 r19.41v 2706 . . . . . 6  |-  ( E. x  e.  A  ( y  =  B  /\  z  e.  y )  <->  ( E. x  e.  A  y  =  B  /\  z  e.  y )
)
109exbii 1572 . . . . 5  |-  ( E. y E. x  e.  A  ( y  =  B  /\  z  e.  y )  <->  E. y
( E. x  e.  A  y  =  B  /\  z  e.  y ) )
11 exancom 1576 . . . . 5  |-  ( E. y ( E. x  e.  A  y  =  B  /\  z  e.  y )  <->  E. y ( z  e.  y  /\  E. x  e.  A  y  =  B ) )
1210, 11bitri 240 . . . 4  |-  ( E. y E. x  e.  A  ( y  =  B  /\  z  e.  y )  <->  E. y
( z  e.  y  /\  E. x  e.  A  y  =  B ) )
138, 12syl6bb 252 . . 3  |-  ( A. x  e.  A  B  e.  C  ->  ( E. x  e.  A  z  e.  B  <->  E. y
( z  e.  y  /\  E. x  e.  A  y  =  B ) ) )
14 eliun 3925 . . 3  |-  ( z  e.  U_ x  e.  A  B  <->  E. x  e.  A  z  e.  B )
15 eluniab 3855 . . 3  |-  ( z  e.  U. { y  |  E. x  e.  A  y  =  B }  <->  E. y ( z  e.  y  /\  E. x  e.  A  y  =  B ) )
1613, 14, 153bitr4g 279 . 2  |-  ( A. x  e.  A  B  e.  C  ->  ( z  e.  U_ x  e.  A  B  <->  z  e.  U. { y  |  E. x  e.  A  y  =  B } ) )
1716eqrdv 2294 1  |-  ( A. x  e.  A  B  e.  C  ->  U_ x  e.  A  B  =  U. { y  |  E. x  e.  A  y  =  B } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556   E.wrex 2557   U.cuni 3843   U_ciun 3921
This theorem is referenced by:  dfiun2  3953  dfiun3g  4947  iunexg  5783  uniqs  6735  ac6num  8122  iunopn  16660  pnrmopn  17087  cncmp  17135  ptcmplem3  17764  iunmbl  18926  voliun  18927  sigaclcuni  23494  sigaclcu2  23496  sigaclci  23508  measvunilem  23555  meascnbl  23561
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-v 2803  df-uni 3844  df-iun 3923
  Copyright terms: Public domain W3C validator