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

Theorem iuneq1 4310
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 4308 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4308 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 568 . 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 3479 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3479 . 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 269 1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    C_ wss 3436   U_ciun 4296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-v 3083  df-in 3443  df-ss 3450  df-iun 4298
This theorem is referenced by:  iuneq1d  4321  iinvdif  4368  iununi  4384  iunsuc  5520  funiunfv  6164  onfununi  7064  iunfi  7864  rankuni2b  8325  pwsdompw  8634  ackbij1lem7  8656  r1om  8674  fictb  8675  cfsmolem  8700  ituniiun  8852  domtriomlem  8872  domtriom  8873  inar1  9200  fsum2d  13817  fsumiun  13866  ackbijnn  13871  fprod2d  14020  prmreclem5  14849  lpival  18454  fiuncmp  20403  ovolfiniun  22438  ovoliunnul  22444  finiunmbl  22481  volfiniun  22484  voliunlem1  22487  iuninc  28163  ofpreima2  28256  esum2dlem  28906  sigaclfu2  28936  sigapildsyslem  28976  fiunelros  28989  bnj548  29701  bnj554  29703  bnj594  29716  trpredlem1  30460  trpredtr  30463  trpredmintr  30464  trpredrec  30471  neibastop2lem  31006  istotbnd3  32014  0totbnd  32016  sstotbnd2  32017  sstotbnd  32018  sstotbnd3  32019  totbndbnd  32032  prdstotbnd  32037  cntotbnd  32039  heibor  32064  dfrcl4  36125  iunrelexp0  36151  comptiunov2i  36155  corclrcl  36156  cotrcltrcl  36174  trclfvdecomr  36177  dfrtrcl4  36187  corcltrcl  36188  cotrclrcl  36191  fiiuncl  37266  sge0iunmptlemfi  38040  caragenfiiuncl  38112  carageniuncllem1  38118  iunxprg  38703  funopsn  38714
  Copyright terms: Public domain W3C validator