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

Theorem iuneq1 4329
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 4327 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4327 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 564 . 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 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3504 . 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 367    = wceq 1398    C_ wss 3461   U_ciun 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-v 3108  df-in 3468  df-ss 3475  df-iun 4317
This theorem is referenced by:  iuneq1d  4340  iinvdif  4387  iununi  4403  iunsuc  4949  funiunfv  6135  onfununi  7004  iunfi  7800  rankuni2b  8262  pwsdompw  8575  ackbij1lem7  8597  r1om  8615  fictb  8616  cfsmolem  8641  ituniiun  8793  domtriomlem  8813  domtriom  8814  inar1  9142  fsum2d  13671  fsumiun  13720  ackbijnn  13725  fprod2d  13870  prmreclem5  14525  lpival  18091  fiuncmp  20074  ovolfiniun  22081  ovoliunnul  22087  finiunmbl  22123  volfiniun  22126  voliunlem1  22129  iuninc  27641  ofpreima2  27738  esum2dlem  28324  sigaclfu2  28354  sigapildsyslem  28390  trpredlem1  29553  trpredtr  29556  trpredmintr  29557  trpredrec  29564  neibastop2lem  30421  istotbnd3  30510  0totbnd  30512  sstotbnd2  30513  sstotbnd  30514  sstotbnd3  30515  totbndbnd  30528  prdstotbnd  30533  cntotbnd  30535  heibor  30560  iunxprg  32695  bnj548  34375  bnj554  34377  bnj594  34390  dfrcl4  38218  dfrtrcl4  38236  comptiunov2i  38237  iunrelexp0  38245  corclrcl  38251  corcltrcl  38252  cotrclrcl  38253  cotrcltrcl  38254
  Copyright terms: Public domain W3C validator