Theorem uneq2d 4119

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 4113	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

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

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 3438  df-un 3908

This theorem is referenced by:  ifeq2  4481  tpeq3  4696  iununi  5048  sucprc  6385  unisucs  6386  resasplit  6694  fvun1  6914  fmptapd  7107  fndifnfp  7112  fvunsn  7115  fnsnsplit  7120  f1ofvswap  7243  oev2  8441  oarec  8480  ralxpmap  8823  sbthlem5  9008  sbthlem6  9009  domss2  9053  dif1en  9075  unfi  9085  fodomfi  9201  domunfican  9211  fiint  9216  fiintOLD  9217  fodomfiOLD  9220  pm54.43  9897  kmlem2  10046  kmlem11  10055  ackbij1lem1  10113  fin23lem26  10219  axdc3lem4  10347  fpwwe2lem12  10536  wunex2  10632  wuncval2  10641  ioounsn  13380  snunico  13382  ioojoin  13386  fzsuc  13474  fseq1p1m1  13501  fseq1m1p1  13502  fzosplitsnm1  13643  fzosplitsn  13678  fzosplitpr  13679  fzosplitprm1  13680  hashfun  14344  resunimafz0  14352  s4prop  14817  fsumm1  15658  climcndslem1  15756  fprodm1  15874  ruclem4  16143  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfunsn  16555  vdwap1  16889  setscom  17091  setsidvald  17110  mreexmrid  17549  mreexexlemd  17550  mreexexlem2d  17551  cnvtsr  18494  dprd2da  19923  dmdprdsplit2lem  19926  lspun0  20914  lbsextlem4  21068  cmpcld  23287  comppfsc  23417  trfil2  23772  cldsubg  23996  tsmsres  24029  icccmplem2  24710  uniioombllem4  25485  ppiprm  27059  chtprm  27061  pntrsumbnd2  27476  noextend  27576  nodenselem5  27598  nosupbnd2lem1  27625  addsproplem1  27881  addsprop  27888  negsproplem1  27939  negsprop  27946  mulsproplemcbv  28023  mulsproplem1  28024  mulsprop  28038  precsexlemcbv  28113  precsexlem3  28116  onsleft  28166  sltonold  28167  onscutlt  28170  pthdlem1  29711  wwlksnext  29838  clwwlknonex2lem1  30051  iunxunsn  32510  iunxunpr  32511  difres  32544  ofpreima2  32609  fzspl  32732  tocyc01  33060  ordtprsuni  33886  ordtcnvNEW  33887  carsgsigalem  34283  ballotlemfp1  34460  fsum2dsub  34575  reprsuc  34583  bnj941  34739  bnj944  34905  fineqvac  35072  subfacp1lem1  35152  cvmscld  35246  satf  35326  satfv1  35336  fmlasuc  35359  mrsubvrs  35495  mclsval  35536  rankaltopb  35953  rankung  36140  lindsadd  37593  lindsenlbs  37595  poimirlem1  37601  poimirlem2  37602  poimirlem4  37604  poimirlem6  37606  poimirlem7  37607  poimirlem8  37608  poimirlem13  37613  poimirlem14  37614  poimirlem16  37616  poimirlem17  37617  poimirlem18  37618  poimirlem19  37619  poimirlem20  37620  poimirlem21  37621  poimirlem22  37622  poimirlem26  37626  poimirlem28  37628  poimirlem31  37631  poimirlem32  37632  lshpnel2N  38964  paddfval  39776  hdmapval  41807  fzsplitnd  41955  lcmfunnnd  41985  fsuppssind  42566  diophren  42786  omabs2  43305  tfsconcatrn  43315  tfsconcatrev  43321  iunrelexp0  43675  trclfvdecoml  43702  isotone1  44021  iunp1  45044  snunioo1  45493  dvmptfprodlem  45925  stoweidlem11  45992  stoweidlem26  46007  fourierdlem33  46121  fzopredsuc  47307  iccpartltu  47409  iccpartgt  47411  dfclnbgr2  47807  dfclnbgr4  47808  dfclnbgr3  47810  clnbupgr  47817  clnbgr0edg  47821  dfclnbgr5  47834  dfclnbgr6  47840  dfsclnbgr6  47842  cycl3grtri  47931  stgrclnbgr0  47949  lmod1zr  48478  tposres2  48864