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

Theorem uneq2d 3611
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
uneq2d  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq2 3605 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    u. cun 3427
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-or 370  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-v 3073  df-un 3434
This theorem is referenced by:  ifeq2  3897  tpeq3  4066  iununi  4356  relcoi1  5467  resasplit  5682  fvun1  5864  fmptapd  6004  fndifnfp  6009  fvunsn  6012  fnsnsplit  6017  oev2  7066  oarec  7104  ralxpmap  7365  sbthlem5  7528  sbthlem6  7529  domss2  7573  domunfican  7688  fiint  7692  fodomfi  7694  pm54.43  8274  kmlem2  8424  kmlem11  8433  cdaval  8443  cdaassen  8455  ackbij1lem1  8493  fin23lem26  8598  axdc3lem4  8726  fpwwe2lem13  8913  wunex2  9009  wuncval2  9018  snunico  11522  ioojoin  11526  fzsuc  11612  fseq1p1m1  11644  fseq1m1p1  11645  fzosplitsnm1  11718  fzosplitsn  11743  hashfun  12310  s4prop  12636  fsumm1  13331  climcndslem1  13423  ruclem4  13627  vdwap1  14149  setscom  14315  mreexmrid  14692  mreexexlemd  14693  mreexexlem2d  14694  cnvtsr  15503  dprd2da  16655  dmdprdsplit2lem  16658  lspun0  17207  lbsextlem4  17357  cmpcld  19130  trfil2  19585  cldsubg  19806  tsmsresOLD  19842  tsmsres  19843  icccmplem2  20525  uniioombllem4  21192  ppiprm  22615  chtprm  22617  pntrsumbnd2  22942  eupath2lem3  23745  ofpreima2  26129  fzspl  26215  ordtprsuni  26487  ballotlemfp1  27011  subfacp1lem1  27204  cvmscld  27299  fprodm1  27614  rankaltopb  28147  rankung  28341  comppfsc  28720  diophren  29293  ioounsn  29726  stoweidlem11  29947  stoweidlem26  29962  fzosplitpr  30364  fzosplitprm1  30365  wwlknext  30497  lmod1zr  31145  bnj941  32069  bnj944  32234  lshpnel2N  32939  paddfval  33750  hdmapval  35785
  Copyright terms: Public domain W3C validator