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

Theorem iuneq1d 3928
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 3918 . 2  |-  ( A  =  B  ->  U_ x  e.  A  C  =  U_ x  e.  B  C
)
31, 2syl 15 1  |-  ( ph  ->  U_ x  e.  A  C  =  U_ x  e.  B  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   U_ciun 3905
This theorem is referenced by:  iuneq12d  3929  disjxiun  4020  kmlem11  7786  prmreclem4  12966  imasval  13414  iundisj  18905  iundisj2  18906  voliunlem1  18907  iunmbl  18910  volsup  18913  uniioombllem4  18941  iuninc  23158  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  iundisjcnt  23367  sigaclcu3  23483  meascnbl  23546  indval2  23598  cvmliftlem10  23825  heiborlem3  26537  heibor  26545  bnj1113  28817  bnj570  28937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-iun 3907
  Copyright terms: Public domain W3C validator