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

Theorem iuneq2i 4334
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 4332 . 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 2806 1  |-  U_ x  e.  A  B  =  U_ x  e.  A  C
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   U_ciun 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-v 3097  df-in 3468  df-ss 3475  df-iun 4317
This theorem is referenced by:  dfiunv2  4351  iunrab  4362  iunid  4370  iunin1  4380  2iunin  4383  resiun1  5282  resiun2  5283  dfimafn2  5908  dfmpt  6061  funiunfv  6145  fpar  6889  onovuni  7015  uniqs  7373  marypha2lem2  7898  alephlim  8451  cfsmolem  8653  ituniiun  8805  imasdsval2  14790  lpival  17767  cmpsublem  19772  txbasval  19980  uniioombllem2  21865  uniioombllem4  21868  volsup2  21887  itg1addlem5  21980  itg1climres  21994  indval2  27901  sigaclfu2  27994  measvuni  28058  trpred0  29294  rabiun  30011  mblfinlem2  30027  voliunnfl  30033  cnambfre  30038  dfaimafn2  32089  xpiun  32292
  Copyright terms: Public domain W3C validator