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

Theorem iuneq2i 4103
Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
Hypothesis
Ref Expression
iuneq2i.1  |-  ( x  e.  A  ->  B  =  C )
Assertion
Ref Expression
iuneq2i  |-  U_ x  e.  A  B  =  U_ x  e.  A  C

Proof of Theorem iuneq2i
StepHypRef Expression
1 iuneq2 4101 . 2  |-  ( A. x  e.  A  B  =  C  ->  U_ x  e.  A  B  =  U_ x  e.  A  C
)
2 iuneq2i.1 . 2  |-  ( x  e.  A  ->  B  =  C )
31, 2mprg 2767 1  |-  U_ x  e.  A  B  =  U_ x  e.  A  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   U_ciun 4085
This theorem is referenced by:  dfiunv2  4119  iunrab  4130  iunid  4138  iunin1  4148  2iunin  4151  resiun1  5157  resiun2  5158  dfimafn2  5768  dfmpt  5903  funiunfv  5987  fpar  6442  onovuni  6596  abianfplem  6707  uniqs  6956  marypha2lem2  7433  alephlim  7940  cfsmolem  8142  ituniiun  8294  imasdsval2  13734  lpival  16308  cmpsublem  17454  txbasval  17630  uniioombllem2  19467  uniioombllem4  19470  volsup2  19489  itg1addlem5  19584  itg1climres  19598  indval2  24404  sigaclfu2  24496  measvuni  24560  trpred0  25506  rabiun2  26230  mblfinlem  26234  voliunnfl  26240  cnambfre  26245  dfaimafn2  27987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-v 2950  df-in 3319  df-ss 3326  df-iun 4087
  Copyright terms: Public domain W3C validator