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

Theorem uneq2d 3620
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 3614 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 17 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    u. cun 3434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441
This theorem is referenced by:  ifeq2  3916  tpeq3  4090  iununi  4387  relcoi1OLD  5384  resasplit  5770  fvun1  5952  fmptapd  6103  fndifnfp  6108  fvunsn  6111  fnsnsplit  6116  oev2  7236  oarec  7274  ralxpmap  7532  sbthlem5  7695  sbthlem6  7696  domss2  7740  domunfican  7853  fiint  7857  fodomfi  7859  pm54.43  8442  kmlem2  8588  kmlem11  8597  cdaval  8607  cdaassen  8619  ackbij1lem1  8657  fin23lem26  8762  axdc3lem4  8890  fpwwe2lem13  9074  wunex2  9170  wuncval2  9179  snunico  11766  ioojoin  11770  fzsuc  11850  fseq1p1m1  11875  fseq1m1p1  11876  fzosplitsnm1  11994  fzosplitsn  12023  fzosplitprm1  12024  hashfun  12613  s4prop  13000  fsumm1  13811  climcndslem1  13906  fprodm1  14020  ruclem4  14285  lcmfunsnlem1  14609  lcmfunsnlem2lem1  14610  lcmfunsnlem2lem2  14611  lcmfunsnlem2  14612  lcmfunsn  14616  vdwap1  14926  setsidvald  15146  setscom  15152  mreexmrid  15548  mreexexlemd  15549  mreexexlem2d  15550  cnvtsr  16467  dprd2da  17674  dmdprdsplit2lem  17677  lspun0  18233  lbsextlem4  18383  cmpcld  20415  comppfsc  20545  trfil2  20900  cldsubg  21123  tsmsres  21156  icccmplem2  21839  uniioombllem4  22542  ppiprm  24076  chtprm  24078  pntrsumbnd2  24403  wwlknext  25450  eupath2lem3  25705  difres  28213  ofpreima2  28271  fzspl  28374  ordtprsuni  28733  ordtcnvNEW  28734  carsgsigalem  29155  ballotlemfp1  29332  bnj941  29592  bnj944  29757  subfacp1lem1  29910  cvmscld  30004  mrsubvrs  30168  mclsval  30209  rankaltopb  30751  rankung  30938  poimirlem1  31905  poimirlem2  31906  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem13  31917  poimirlem14  31918  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem26  31930  poimirlem28  31932  poimirlem31  31935  poimirlem32  31936  lshpnel2N  32520  paddfval  33331  hdmapval  35368  diophren  35625  ioounsn  36064  iunrelexp0  36264  trclfvdecoml  36291  iunp1  37380  snunioo2  37555  snunioo1  37562  dvmptfprodlem  37759  stoweidlem11  37811  stoweidlem26  37826  fourierdlem33  37943  fzopredsuc  38590  iccpartltu  38609  iccpartgt  38611  fzosplitpr  38919  lmod1zr  39907
  Copyright terms: Public domain W3C validator