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

Theorem iuneq1 4292
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 4290 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4290 . . 3  |-  ( B 
C_  A  ->  U_ x  e.  B  C  C_  U_ x  e.  A  C )
31, 2anim12i 570 . 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 3447 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3447 . 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 270 1  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    C_ wss 3404   U_ciun 4278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-v 3047  df-in 3411  df-ss 3418  df-iun 4280
This theorem is referenced by:  iuneq1d  4303  iinvdif  4350  iununi  4366  iunsuc  5505  funiunfv  6153  onfununi  7060  iunfi  7862  rankuni2b  8324  pwsdompw  8634  ackbij1lem7  8656  r1om  8674  fictb  8675  cfsmolem  8700  ituniiun  8852  domtriomlem  8872  domtriom  8873  inar1  9200  fsum2d  13832  fsumiun  13881  ackbijnn  13886  fprod2d  14035  prmreclem5  14864  lpival  18469  fiuncmp  20419  ovolfiniun  22454  ovoliunnul  22460  finiunmbl  22497  volfiniun  22500  voliunlem1  22503  iuninc  28176  ofpreima2  28269  esum2dlem  28913  sigaclfu2  28943  sigapildsyslem  28983  fiunelros  28996  bnj548  29708  bnj554  29710  bnj594  29723  trpredlem1  30468  trpredtr  30471  trpredmintr  30472  trpredrec  30479  neibastop2lem  31016  istotbnd3  32103  0totbnd  32105  sstotbnd2  32106  sstotbnd  32107  sstotbnd3  32108  totbndbnd  32121  prdstotbnd  32126  cntotbnd  32128  heibor  32153  dfrcl4  36268  iunrelexp0  36294  comptiunov2i  36298  corclrcl  36299  cotrcltrcl  36317  trclfvdecomr  36320  dfrtrcl4  36330  corcltrcl  36331  cotrclrcl  36334  fiiuncl  37406  sge0iunmptlemfi  38255  caragenfiiuncl  38336  carageniuncllem1  38342  iunxprg  39004  funopsn  39018
  Copyright terms: Public domain W3C validator