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

Theorem iuneq1 3918
Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
iuneq1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    C( x)

Proof of Theorem iuneq1
StepHypRef Expression
1 iunss1 3916 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 3916 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( U_ x  e.  A  C  C_  U_ x  e.  B  C  /\  U_ x  e.  B  C  C_ 
U_ x  e.  A  C ) )
4 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3194 . 2  |-  ( U_ x  e.  A  C  =  U_ x  e.  B  C 
<->  ( U_ x  e.  A  C  C_  U_ x  e.  B  C  /\  U_ x  e.  B  C  C_ 
U_ x  e.  A  C ) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    C_ wss 3152   U_ciun 3905
This theorem is referenced by:  iuneq1d  3928  iununi  3986  iunsuc  4474  funiunfv  5774  onfununi  6358  iunfi  7144  rankuni2b  7525  pwsdompw  7830  ackbij1lem7  7852  r1om  7870  fictb  7871  cfsmolem  7896  ituniiun  8048  domtriomlem  8068  domtriom  8069  inar1  8397  fsum2d  12234  fsumiun  12279  ackbijnn  12286  prmreclem5  12967  lpival  15997  fiuncmp  17131  ovolfiniun  18860  ovoliunnul  18866  finiunmbl  18901  volfiniun  18904  voliunlem1  18907  iuninc  23158  sigaclfu2  23482  trpredlem1  24230  trpredtr  24233  trpredmintr  24234  trpredrec  24241  neibastop2lem  26309  istotbnd3  26495  0totbnd  26497  sstotbnd2  26498  sstotbnd  26499  sstotbnd3  26500  totbndbnd  26513  prdstotbnd  26518  cntotbnd  26520  heibor  26545  bnj548  28929  bnj554  28931  bnj594  28944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-iun 3907
  Copyright terms: Public domain W3C validator