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

Theorem iuneq2i 4344
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 4342 . 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 2827 1  |-  U_ x  e.  A  B  =  U_ x  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   U_ciun 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327
This theorem is referenced by:  dfiunv2  4361  iunrab  4372  iunid  4380  iunin1  4390  2iunin  4393  resiun1  5290  resiun2  5291  dfimafn2  5915  dfmpt  6064  funiunfv  6146  fpar  6884  onovuni  7010  uniqs  7368  marypha2lem2  7892  alephlim  8444  cfsmolem  8646  ituniiun  8798  imasdsval2  14767  lpival  17675  cmpsublem  19665  txbasval  19842  uniioombllem2  21727  uniioombllem4  21730  volsup2  21749  itg1addlem5  21842  itg1climres  21856  indval2  27668  sigaclfu2  27761  measvuni  27825  trpred0  28896  rabiun  29613  mblfinlem2  29629  voliunnfl  29635  cnambfre  29640  dfaimafn2  31718
  Copyright terms: Public domain W3C validator