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

Theorem uneq2d 3585
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 3579 . 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 1399    u. cun 3400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-v 3049  df-un 3407
This theorem is referenced by:  ifeq2  3875  tpeq3  4047  iununi  4344  relcoi1OLD  5458  resasplit  5676  fvun1  5858  fmptapd  6011  fndifnfp  6016  fvunsn  6019  fnsnsplit  6024  oev2  7109  oarec  7147  ralxpmap  7405  sbthlem5  7568  sbthlem6  7569  domss2  7613  domunfican  7726  fiint  7730  fodomfi  7732  pm54.43  8312  kmlem2  8462  kmlem11  8471  cdaval  8481  cdaassen  8493  ackbij1lem1  8531  fin23lem26  8636  axdc3lem4  8764  fpwwe2lem13  8949  wunex2  9045  wuncval2  9054  snunico  11586  ioojoin  11590  fzsuc  11667  fseq1p1m1  11692  fseq1m1p1  11693  fzosplitsnm1  11807  fzosplitsn  11836  fzosplitprm1  11837  hashfun  12418  s4prop  12793  fsumm1  13587  climcndslem1  13682  fprodm1  13792  ruclem4  13988  vdwap1  14516  setsidvald  14679  setscom  14685  mreexmrid  15069  mreexexlemd  15070  mreexexlem2d  15071  cnvtsr  15988  dprd2da  17223  dmdprdsplit2lem  17226  lspun0  17789  lbsextlem4  17939  cmpcld  20007  comppfsc  20137  trfil2  20492  cldsubg  20713  tsmsresOLD  20749  tsmsres  20750  icccmplem2  21432  uniioombllem4  22099  ppiprm  23561  chtprm  23563  pntrsumbnd2  23888  wwlknext  24866  eupath2lem3  25121  difres  27620  ofpreima2  27684  fzspl  27781  ordtprsuni  28086  ordtcnvNEW  28087  carsgsigalem  28478  ballotlemfp1  28649  subfacp1lem1  28848  cvmscld  28943  mrsubvrs  29107  mclsval  29148  rankaltopb  29818  rankung  30012  diophren  30948  ioounsn  31381  snunioo2  31745  snunioo1  31753  dvmptfprodlem  31942  stoweidlem11  31994  stoweidlem26  32009  fourierdlem33  32123  fzosplitpr  32697  lmod1zr  33329  bnj941  34213  bnj944  34378  lshpnel2N  35158  paddfval  35969  hdmapval  38006  iunrelexp0  38277
  Copyright terms: Public domain W3C validator