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

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

Proof of Theorem iuneq12d
StepHypRef Expression
1 iuneq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21iuneq1d 4327 . 2  |-  ( ph  ->  U_ x  e.  A  C  =  U_ x  e.  B  C )
3 iuneq12d.2 . . . 4  |-  ( ph  ->  C  =  D )
43adantr 466 . . 3  |-  ( (
ph  /\  x  e.  B )  ->  C  =  D )
54iuneq2dv 4324 . 2  |-  ( ph  ->  U_ x  e.  B  C  =  U_ x  e.  B  D )
62, 5eqtrd 2470 1  |-  ( ph  ->  U_ x  e.  A  C  =  U_ x  e.  B  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870   U_ciun 4302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-v 3089  df-in 3449  df-ss 3456  df-iun 4304
This theorem is referenced by:  otiunsndisj  4727  cfsmolem  8698  cfsmo  8699  wunex2  9162  wuncval2  9171  imasval  15359  lpival  18395  cnextval  20998  cnextfval  20999  dvfval  22720  2spotiundisj  25626  mblfinlem2  31672  heiborlem10  31846  iunrelexpmin1  35929  iunrelexpmin2  35933
  Copyright terms: Public domain W3C validator