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

Theorem iuneq1 4339
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 4337 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4337 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 566 . 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 3519 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3519 . 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 266 1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    C_ wss 3476   U_ciun 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327
This theorem is referenced by:  iuneq1d  4350  iinvdif  4397  iununi  4410  iunsuc  4960  funiunfv  6148  onfununi  7012  iunfi  7808  rankuni2b  8271  pwsdompw  8584  ackbij1lem7  8606  r1om  8624  fictb  8625  cfsmolem  8650  ituniiun  8802  domtriomlem  8822  domtriom  8823  inar1  9153  fsum2d  13549  fsumiun  13598  ackbijnn  13603  prmreclem5  14297  lpival  17692  fiuncmp  19698  ovolfiniun  21675  ovoliunnul  21681  finiunmbl  21717  volfiniun  21720  voliunlem1  21723  iuninc  27129  ofpreima2  27208  sigaclfu2  27789  fprod2d  28716  trpredlem1  28915  trpredtr  28918  trpredmintr  28919  trpredrec  28926  neibastop2lem  29809  istotbnd3  29898  0totbnd  29900  sstotbnd2  29901  sstotbnd  29902  sstotbnd3  29903  totbndbnd  29916  prdstotbnd  29921  cntotbnd  29923  heibor  29948  iunxprg  31797  bnj548  33052  bnj554  33054  bnj594  33067
  Copyright terms: Public domain W3C validator