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

Theorem iuneq1d 4118
Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
Hypothesis
Ref Expression
iuneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
iuneq1d  |-  ( ph  ->  U_ x  e.  A  C  =  U_ x  e.  B  C )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem iuneq1d
StepHypRef Expression
1 iuneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 iuneq1 4108 . 2  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
31, 2syl 16 1  |-  ( ph  ->  U_ x  e.  A  C  =  U_ x  e.  B  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   U_ciun 4095
This theorem is referenced by:  iuneq12d  4119  disjxiun  4212  kmlem11  8045  prmreclem4  13292  imasval  13742  iundisj  19447  iundisj2  19448  voliunlem1  19449  iunmbl  19452  volsup  19455  uniioombllem4  19483  iuninc  24016  iundisjf  24034  iundisj2f  24035  iundisjfi  24157  iundisj2fi  24158  iundisjcnt  24159  indval2  24417  sigaclcu3  24510  meascnbl  24578  cvmliftlem10  24986  voliunnfl  26262  volsupnfl  26263  heiborlem3  26536  heibor  26544  bnj1113  29230  bnj155  29324  bnj570  29350  bnj893  29373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-iun 4097
  Copyright terms: Public domain W3C validator