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

Theorem iuneq2dv 4058
Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
Hypothesis
Ref Expression
iuneq2dv.1  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
Assertion
Ref Expression
iuneq2dv  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)

Proof of Theorem iuneq2dv
StepHypRef Expression
1 iuneq2dv.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
21ralrimiva 2734 . 2  |-  ( ph  ->  A. x  e.  A  B  =  C )
3 iuneq2 4053 . 2  |-  ( A. x  e.  A  B  =  C  ->  U_ x  e.  A  B  =  U_ x  e.  A  C
)
42, 3syl 16 1  |-  ( ph  ->  U_ x  e.  A  B  =  U_ x  e.  A  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2651   U_ciun 4037
This theorem is referenced by:  iuneq12d  4061  iuneq2d  4062  fparlem3  6389  fparlem4  6390  oalim  6714  omlim  6715  oelim  6716  oelim2  6776  r1val3  7699  imasdsval  13670  acsfn  13813  tgidm  16970  cmpsub  17387  alexsublem  17998  bcth3  19155  ovoliunlem1  19267  voliunlem1  19313  uniiccdif  19339  uniioombllem2  19344  uniioombllem3a  19345  uniioombllem4  19347  itg2monolem1  19511  taylpfval  20150  cvmscld  24741  heibor  26223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-rex 2657  df-v 2903  df-in 3272  df-ss 3279  df-iun 4039
  Copyright terms: Public domain W3C validator