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

Theorem iuneq1 3934
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 3932 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 3932 . . 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 3207 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3207 . 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 1632    C_ wss 3165   U_ciun 3921
This theorem is referenced by:  iuneq1d  3944  iununi  4002  iunsuc  4490  funiunfv  5790  onfununi  6374  iunfi  7160  rankuni2b  7541  pwsdompw  7846  ackbij1lem7  7868  r1om  7886  fictb  7887  cfsmolem  7912  ituniiun  8064  domtriomlem  8084  domtriom  8085  inar1  8413  fsum2d  12250  fsumiun  12295  ackbijnn  12302  prmreclem5  12983  lpival  16013  fiuncmp  17147  ovolfiniun  18876  ovoliunnul  18882  finiunmbl  18917  volfiniun  18920  voliunlem1  18923  iuninc  23174  sigaclfu2  23497  trpredlem1  24301  trpredtr  24304  trpredmintr  24305  trpredrec  24312  neibastop2lem  26412  istotbnd3  26598  0totbnd  26600  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  totbndbnd  26616  prdstotbnd  26621  cntotbnd  26623  heibor  26648  bnj548  29245  bnj554  29247  bnj594  29260
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-in 3172  df-ss 3179  df-iun 3923
  Copyright terms: Public domain W3C validator