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

Theorem iuneq1d 4293
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 4282 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1370   U_ciun 4269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-v 3070  df-in 3433  df-ss 3440  df-iun 4271
This theorem is referenced by:  iuneq12d  4294  disjxiun  4387  kmlem11  8430  prmreclem4  14082  imasval  14551  iundisj  21145  iundisj2  21146  voliunlem1  21147  iunmbl  21150  volsup  21153  uniioombllem4  21182  iuninc  26045  iundisjf  26065  iundisj2f  26066  iundisjfi  26214  iundisj2fi  26215  iundisjcnt  26216  indval2  26605  sigaclcu3  26699  meascnbl  26767  cvmliftlem10  27317  voliunnfl  28573  volsupnfl  28574  heiborlem3  28850  heibor  28858  bnj1113  32079  bnj155  32172  bnj570  32198  bnj893  32221
  Copyright terms: Public domain W3C validator