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

Theorem iuneq1 4107
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 4105 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4105 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 551 . 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 3364 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3364 . 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 259 1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    C_ wss 3321   U_ciun 4094
This theorem is referenced by:  iuneq1d  4117  iununi  4176  iunsuc  4664  funiunfv  5996  onfununi  6604  iunfi  7395  rankuni2b  7780  pwsdompw  8085  ackbij1lem7  8107  r1om  8125  fictb  8126  cfsmolem  8151  ituniiun  8303  domtriomlem  8323  domtriom  8324  inar1  8651  fsum2d  12556  fsumiun  12601  ackbijnn  12608  prmreclem5  13289  lpival  16317  fiuncmp  17468  ovolfiniun  19398  ovoliunnul  19404  finiunmbl  19439  volfiniun  19442  voliunlem1  19445  iuninc  24012  sigaclfu2  24505  sibfof  24655  fprod2d  25306  trpredlem1  25506  trpredtr  25509  trpredmintr  25510  trpredrec  25517  neibastop2lem  26390  istotbnd3  26481  0totbnd  26483  sstotbnd2  26484  sstotbnd  26485  sstotbnd3  26486  totbndbnd  26499  prdstotbnd  26504  cntotbnd  26506  heibor  26531  iunxprg  28069  bnj548  29269  bnj554  29271  bnj594  29284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rex 2712  df-v 2959  df-in 3328  df-ss 3335  df-iun 4096
  Copyright terms: Public domain W3C validator