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

Theorem uneq12d 3494
Description: Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Hypotheses
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
uneq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
uneq12d  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )

Proof of Theorem uneq12d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 uneq12 3488 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3310
This theorem is referenced by:  disjpr2  3862  diftpsn3  3929  suceq  4638  fntpg  5498  foun  5685  f1oprswap  5709  fnimapr  5779  fsnunfv  5925  fsnunres  5926  oarec  6797  ereq1  6904  mapunen  7268  cnfcomlem  7646  trcl  7654  r0weon  7884  infxpen  7886  cfsmolem  8140  cfsmo  8141  axdc3lem4  8323  ttukeylem3  8381  ttukey2g  8386  alephadd  8442  fpwwe2lem13  8507  wunex2  8603  wuncval2  8612  inar1  8640  prunioo  11015  fztp  11092  fzsuc2  11094  fseq1p1m1  11112  s4dom  11856  setsvalg  13482  setsid  13498  prdsval  13668  imasval  13727  mreexd  13857  mreexexlemd  13859  ipoval  14570  istsr  14639  psrval  16419  ordtval  17243  ordtcnv  17255  paste  17348  consuba  17473  ptval2  17623  dfac14  17640  xkoptsub  17676  ptuncnv  17829  ptunhmeo  17830  xpstopnlem1  17831  alexsubALTlem3  18070  ustuqtop1  18261  ovolioo  19452  uniiccdif  19460  itgsplitioo  19719  limcfval  19749  lhop2  19889  lgsquadlem2  21129  constr2spthlem1  21584  constr3pthlem1  21632  constr3pthlem2  21633  vdgrun  21662  vdgrfiun  21663  ex-res  21739  rnpropg  24025  imadifxp  24028  probun  24667  cvmliftlem10  24971  sbcung  25114  dfrtrcl2  25138  symdifeq1  25630  axlowdimlem13  25858  axlowdimlem15  25860  axlowdim  25865  lineunray  26046  mblfinlem  26207  itg2addnclem2  26220  istopclsd  26708  fzsplit1nn0  26766  diophrw  26771  eldioph2lem1  26772  eldioph2lem2  26773  diophin  26785  diophren  26828  pwssplit1  27120  pwssplit4  27123  mendval  27423  iunxprg  28022  bnj1373  29300  bnj1489  29326  ldualset  29824  paddval  30496  paddcom  30511  dvafset  31702  dvaset  31703  dvhfset  31779  dvhset  31780  hdmapfval  32529  hlhilset  32636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317
  Copyright terms: Public domain W3C validator