Theorem uneq2d 4131

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq2d	⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq2 4125	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  ifeq2  4493  tpeq3  4708  iununi  5063  sucprc  6410  unisucs  6411  resasplit  6730  fvun1  6952  fmptapd  7145  fndifnfp  7150  fvunsn  7153  fnsnsplit  7158  f1ofvswap  7281  oev2  8487  oarec  8526  ralxpmap  8869  sbthlem5  9055  sbthlem6  9056  domss2  9100  dif1en  9124  dif1enOLD  9126  unfi  9135  fodomfi  9261  domunfican  9272  fiint  9277  fiintOLD  9278  fodomfiOLD  9281  pm54.43  9954  kmlem2  10105  kmlem11  10114  ackbij1lem1  10172  fin23lem26  10278  axdc3lem4  10406  fpwwe2lem12  10595  wunex2  10691  wuncval2  10700  ioounsn  13438  snunico  13440  ioojoin  13444  fzsuc  13532  fseq1p1m1  13559  fseq1m1p1  13560  fzosplitsnm1  13701  fzosplitsn  13736  fzosplitpr  13737  fzosplitprm1  13738  hashfun  14402  resunimafz0  14410  s4prop  14876  fsumm1  15717  climcndslem1  15815  fprodm1  15933  ruclem4  16202  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfunsn  16614  vdwap1  16948  setscom  17150  setsidvald  17169  mreexmrid  17604  mreexexlemd  17605  mreexexlem2d  17606  cnvtsr  18547  dprd2da  19974  dmdprdsplit2lem  19977  lspun0  20917  lbsextlem4  21071  cmpcld  23289  comppfsc  23419  trfil2  23774  cldsubg  23998  tsmsres  24031  icccmplem2  24712  uniioombllem4  25487  ppiprm  27061  chtprm  27063  pntrsumbnd2  27478  noextend  27578  nodenselem5  27600  nosupbnd2lem1  27627  addsproplem1  27876  addsprop  27883  negsproplem1  27934  negsprop  27941  mulsproplemcbv  28018  mulsproplem1  28019  mulsprop  28033  precsexlemcbv  28108  precsexlem3  28111  onsleft  28161  sltonold  28162  onscutlt  28165  pthdlem1  29696  wwlksnext  29823  clwwlknonex2lem1  30036  iunxunsn  32495  iunxunpr  32496  difres  32529  ofpreima2  32590  fzspl  32712  tocyc01  33075  ordtprsuni  33909  ordtcnvNEW  33910  carsgsigalem  34306  ballotlemfp1  34483  fsum2dsub  34598  reprsuc  34606  bnj941  34762  bnj944  34928  fineqvac  35087  subfacp1lem1  35166  cvmscld  35260  satf  35340  satfv1  35350  fmlasuc  35373  mrsubvrs  35509  mclsval  35550  rankaltopb  35967  rankung  36154  lindsadd  37607  lindsenlbs  37609  poimirlem1  37615  poimirlem2  37616  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem26  37640  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  lshpnel2N  38978  paddfval  39791  hdmapval  41822  fzsplitnd  41970  lcmfunnnd  42000  fsuppssind  42581  diophren  42801  omabs2  43321  tfsconcatrn  43331  tfsconcatrev  43337  iunrelexp0  43691  trclfvdecoml  43718  isotone1  44037  iunp1  45060  snunioo1  45510  dvmptfprodlem  45942  stoweidlem11  46009  stoweidlem26  46024  fourierdlem33  46138  fzopredsuc  47324  iccpartltu  47426  iccpartgt  47428  dfclnbgr2  47824  dfclnbgr4  47825  dfclnbgr3  47827  clnbupgr  47834  clnbgr0edg  47837  dfclnbgr5  47850  dfclnbgr6  47856  dfsclnbgr6  47858  cycl3grtri  47946  stgrclnbgr0  47964  lmod1zr  48482  tposres2  48868