Theorem uneq2d 4122

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  ifeq2  4486  tpeq3  4703  iununi  5056  sucprc  6403  unisucs  6404  resasplit  6712  fvun1  6933  fmptapd  7127  fndifnfp  7132  fvunsn  7135  fnsnsplit  7140  f1ofvswap  7262  oev2  8460  oarec  8499  ralxpmap  8846  sbthlem5  9031  sbthlem6  9032  domss2  9076  dif1en  9098  unfi  9107  fodomfi  9224  domunfican  9234  fiint  9239  fodomfiOLD  9242  pm54.43  9925  kmlem2  10074  kmlem11  10083  ackbij1lem1  10141  fin23lem26  10247  axdc3lem4  10375  fpwwe2lem12  10565  wunex2  10661  wuncval2  10670  ioounsn  13405  snunico  13407  ioojoin  13411  fzsuc  13499  fseq1p1m1  13526  fseq1m1p1  13527  fzosplitsnm1  13668  fzosplitsn  13704  fzosplitpr  13705  fzosplitprm1  13706  hashfun  14372  resunimafz0  14380  s4prop  14845  fsumm1  15686  climcndslem1  15784  fprodm1  15902  ruclem4  16171  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfunsn  16583  vdwap1  16917  setscom  17119  setsidvald  17138  mreexmrid  17578  mreexexlemd  17579  mreexexlem2d  17580  cnvtsr  18523  dprd2da  19985  dmdprdsplit2lem  19988  lspun0  20974  lbsextlem4  21128  cmpcld  23358  comppfsc  23488  trfil2  23843  cldsubg  24067  tsmsres  24100  icccmplem2  24780  uniioombllem4  25555  ppiprm  27129  chtprm  27131  pntrsumbnd2  27546  noextend  27646  nodenselem5  27668  nosupbnd2lem1  27695  addsproplem1  27977  addsprop  27984  negsproplem1  28036  negsprop  28043  mulsproplemcbv  28123  mulsproplem1  28124  mulsprop  28138  precsexlemcbv  28214  precsexlem3  28217  onleft  28268  ltonold  28269  oncutlt  28272  pthdlem1  29851  wwlksnext  29978  clwwlknonex2lem1  30194  iunxunsn  32653  iunxunpr  32654  difres  32687  ofpreima2  32756  fzspl  32880  indconst1  32951  tocyc01  33212  esplyind  33752  ordtprsuni  34097  ordtcnvNEW  34098  carsgsigalem  34493  ballotlemfp1  34670  fsum2dsub  34785  reprsuc  34793  bnj941  34949  bnj944  35114  fineqvac  35294  subfacp1lem1  35395  cvmscld  35489  satf  35569  satfv1  35579  fmlasuc  35602  mrsubvrs  35738  mclsval  35779  rankaltopb  36195  rankung  36382  lindsadd  37864  lindsenlbs  37866  poimirlem1  37872  poimirlem2  37873  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem13  37884  poimirlem14  37885  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem26  37897  poimirlem28  37899  poimirlem31  37902  poimirlem32  37903  lshpnel2N  39361  paddfval  40173  hdmapval  42204  fzsplitnd  42352  lcmfunnnd  42382  fsuppssind  42951  diophren  43170  omabs2  43689  tfsconcatrn  43699  tfsconcatrev  43705  iunrelexp0  44058  trclfvdecoml  44085  isotone1  44404  iunp1  45426  snunioo1  45872  dvmptfprodlem  46302  stoweidlem11  46369  stoweidlem26  46384  fourierdlem33  46498  fzopredsuc  47683  iccpartltu  47785  iccpartgt  47787  dfclnbgr2  48183  dfclnbgr4  48184  dfclnbgr3  48186  clnbupgr  48193  clnbgr0edg  48197  dfclnbgr5  48210  dfclnbgr6  48216  dfsclnbgr6  48218  cycl3grtri  48307  stgrclnbgr0  48325  lmod1zr  48853  tposres2  49239