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

Theorem iuneq1 4182
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 4180 . . 3  |-  ( A 
C_  B  ->  U_ x  e.  A  C  C_  U_ x  e.  B  C )
2 iunss1 4180 . . 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 3369 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3369 . 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 1369    C_ wss 3326   U_ciun 4169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-v 2972  df-in 3333  df-ss 3340  df-iun 4171
This theorem is referenced by:  iuneq1d  4193  iinvdif  4240  iununi  4253  iunsuc  4799  funiunfv  5963  onfununi  6800  iunfi  7597  rankuni2b  8058  pwsdompw  8371  ackbij1lem7  8393  r1om  8411  fictb  8412  cfsmolem  8437  ituniiun  8589  domtriomlem  8609  domtriom  8610  inar1  8940  fsum2d  13236  fsumiun  13282  ackbijnn  13289  prmreclem5  13979  lpival  17325  fiuncmp  19005  ovolfiniun  20982  ovoliunnul  20988  finiunmbl  21023  volfiniun  21026  voliunlem1  21029  iuninc  25909  ofpreima2  25983  sigaclfu2  26562  fprod2d  27490  trpredlem1  27689  trpredtr  27692  trpredmintr  27693  trpredrec  27700  neibastop2lem  28578  istotbnd3  28667  0totbnd  28669  sstotbnd2  28670  sstotbnd  28671  sstotbnd3  28672  totbndbnd  28685  prdstotbnd  28690  cntotbnd  28692  heibor  28717  iunxprg  30131  bnj548  31887  bnj554  31889  bnj594  31902
  Copyright terms: Public domain W3C validator