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

Theorem iuneq1d 4084
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 4074 . 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 1649   U_ciun 4061
This theorem is referenced by:  iuneq12d  4085  disjxiun  4177  kmlem11  8004  prmreclem4  13250  imasval  13700  iundisj  19403  iundisj2  19404  voliunlem1  19405  iunmbl  19408  volsup  19411  uniioombllem4  19439  iuninc  23972  iundisjf  23990  iundisj2f  23991  iundisjfi  24113  iundisj2fi  24114  iundisjcnt  24115  indval2  24373  sigaclcu3  24466  meascnbl  24534  cvmliftlem10  24942  voliunnfl  26157  volsupnfl  26158  heiborlem3  26420  heibor  26428  bnj1113  28874  bnj155  28968  bnj570  28994  bnj893  29017
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680  df-v 2926  df-in 3295  df-ss 3302  df-iun 4063
  Copyright terms: Public domain W3C validator