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

Theorem uneq12d 3659
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 3653 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  csbun  3857  csbungOLD  3858  csbprg  4087  disjpr2  4090  diftpsn3  4165  suceq  4943  rnpropg  5488  fntpg  5643  foun  5834  f1oprswap  5855  fnimapr  5932  residpr  6066  fsnunfv  6102  fsnunres  6103  oarec  7212  ereq1  7319  mapunen  7687  cnfcomlem  8144  cnfcomlemOLD  8152  trcl  8160  r0weon  8391  infxpen  8393  cfsmolem  8651  cfsmo  8652  axdc3lem4  8834  ttukeylem3  8892  ttukey2g  8897  alephadd  8953  fpwwe2lem13  9021  wunex2  9117  wuncval2  9126  inar1  9154  prunioo  11650  fztp  11737  fzsuc2  11738  fseq1p1m1  11753  s4dom  12833  setsvalg  14516  setsid  14534  prdsval  14713  imasval  14769  mreexd  14900  mreexexlemd  14902  ipoval  15644  istsr  15707  gsumzaddlem  16749  pwssplit1  17517  psrval  17822  ordtval  19496  ordtcnv  19508  paste  19601  consuba  19727  ptval2  19929  dfac14  19946  xkoptsub  19982  ptuncnv  20135  ptunhmeo  20136  xpstopnlem1  20137  alexsubALTlem3  20376  ustuqtop1  20571  rrxmvallem  21658  ovolioo  21805  uniiccdif  21814  itgsplitioo  22071  limcfval  22103  lhop2  22243  lgsquadlem2  23455  axlowdimlem13  24030  axlowdimlem15  24032  axlowdim  24037  eengv  24055  constr2spthlem1  24369  constr3pthlem1  24428  constr3pthlem2  24429  vdgrun  24674  vdgrfiun  24675  ex-res  24936  imadifxp  27228  resf1o  27322  ordtprsval  27651  ordtprsuni  27652  ordtcnvNEW  27653  eulerpartlemt  28061  sseqval  28078  probun  28109  cvmliftlem10  28490  mrexval  28612  mrsubffval  28618  msrval  28649  mthmpps  28693  dfrtrcl2  28822  symdifeq1  29323  lineunray  29650  finixpnum  29891  ptrest  29901  mblfinlem2  29905  itg2addnclem2  29920  istopclsd  30463  fzsplit1nn0  30518  diophrw  30523  eldioph2lem1  30524  eldioph2lem2  30525  diophin  30537  diophren  30578  pwssplit4  30866  mendval  30964  iocunico  31010  iunxprg  31996  xpprsng  32216  mndpsuppss  32262  bnj1373  33382  bnj1489  33408  ldualset  34139  paddval  34811  paddcom  34826  dvafset  36017  dvaset  36018  dvhfset  36094  dvhset  36095  hdmapfval  36844  hlhilset  36951
  Copyright terms: Public domain W3C validator