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

Theorem iuneq2i 4310
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 4308 . 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 2762 1  |-  U_ x  e.  A  B  =  U_ x  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    e. wcel 1897   U_ciun 4291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-in 3422  df-ss 3429  df-iun 4293
This theorem is referenced by:  dfiunv2  4327  iunrab  4338  iunid  4346  iunin1  4356  2iunin  4359  resiun1  5141  resiun2  5142  dfimafn2  5937  dfmpt  6092  funiunfv  6177  fpar  6926  onovuni  7086  uniqs  7448  marypha2lem2  7975  alephlim  8523  cfsmolem  8725  ituniiun  8877  imasdsval2  15465  imasdsval2OLD  15477  lpival  18517  cmpsublem  20462  txbasval  20669  uniioombllem2  22588  uniioombllem2OLD  22589  uniioombllem4  22592  volsup2  22611  itg1addlem5  22706  itg1climres  22720  indval2  28884  sigaclfu2  28991  measvuni  29084  trpred0  30525  rabiun  31970  mblfinlem2  32022  voliunnfl  32028  cnambfre  32033  trclrelexplem  36347  cotrclrcl  36378  hoicvr  38407  hoidmv1le  38453  hoidmvle  38459  hspmbllem2  38486  dfaimafn2  38705  xpiun  40038
  Copyright terms: Public domain W3C validator