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

Theorem dfiun2g 4364
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 2838 . . . . . 6  |-  F/ x A. x  e.  A  B  e.  C
2 rsp 2823 . . . . . . . 8  |-  ( A. x  e.  A  B  e.  C  ->  ( x  e.  A  ->  B  e.  C ) )
3 clel3g 3237 . . . . . . . 8  |-  ( B  e.  C  ->  (
z  e.  B  <->  E. y
( y  =  B  /\  z  e.  y ) ) )
42, 3syl6 33 . . . . . . 7  |-  ( A. x  e.  A  B  e.  C  ->  ( x  e.  A  ->  (
z  e.  B  <->  E. y
( y  =  B  /\  z  e.  y ) ) ) )
54imp 429 . . . . . 6  |-  ( ( A. x  e.  A  B  e.  C  /\  x  e.  A )  ->  ( z  e.  B  <->  E. y ( y  =  B  /\  z  e.  y ) ) )
61, 5rexbida 2963 . . . . 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 3129 . . . . 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 261 . . . 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 3009 . . . . . 6  |-  ( E. x  e.  A  ( y  =  B  /\  z  e.  y )  <->  ( E. x  e.  A  y  =  B  /\  z  e.  y )
)
109exbii 1668 . . . . 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 1672 . . . . 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 249 . . . 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 261 . . 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 4337 . . 3  |-  ( z  e.  U_ x  e.  A  B  <->  E. x  e.  A  z  e.  B )
15 eluniab 4262 . . 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 288 . 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 2454 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395   E.wex 1613    e. wcel 1819   {cab 2442   A.wral 2807   E.wrex 2808   U.cuni 4251   U_ciun 4332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-uni 4252  df-iun 4334
This theorem is referenced by:  dfiun2  4366  dfiun3g  5265  iunexg  6775  uniqs  7389  ac6num  8876  iunopn  19534  pnrmopn  19971  cncmp  20019  ptcmplem3  20680  iunmbl  22089  voliun  22090  sigaclcuni  28291  sigaclcu2  28293  sigaclci  28305  measvunilem  28356  meascnbl  28363  carsgclctunlem3  28462
  Copyright terms: Public domain W3C validator