Theorem uneq2d 4134

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  ifeq2  4496  tpeq3  4711  iununi  5066  sucprc  6413  unisucs  6414  resasplit  6733  fvun1  6955  fmptapd  7148  fndifnfp  7153  fvunsn  7156  fnsnsplit  7161  f1ofvswap  7284  oev2  8490  oarec  8529  ralxpmap  8872  sbthlem5  9061  sbthlem6  9062  domss2  9106  dif1en  9130  dif1enOLD  9132  unfi  9141  fodomfi  9268  domunfican  9279  fiint  9284  fiintOLD  9285  fodomfiOLD  9288  pm54.43  9961  kmlem2  10112  kmlem11  10121  ackbij1lem1  10179  fin23lem26  10285  axdc3lem4  10413  fpwwe2lem12  10602  wunex2  10698  wuncval2  10707  ioounsn  13445  snunico  13447  ioojoin  13451  fzsuc  13539  fseq1p1m1  13566  fseq1m1p1  13567  fzosplitsnm1  13708  fzosplitsn  13743  fzosplitpr  13744  fzosplitprm1  13745  hashfun  14409  resunimafz0  14417  s4prop  14883  fsumm1  15724  climcndslem1  15822  fprodm1  15940  ruclem4  16209  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  lcmfunsn  16621  vdwap1  16955  setscom  17157  setsidvald  17176  mreexmrid  17611  mreexexlemd  17612  mreexexlem2d  17613  cnvtsr  18554  dprd2da  19981  dmdprdsplit2lem  19984  lspun0  20924  lbsextlem4  21078  cmpcld  23296  comppfsc  23426  trfil2  23781  cldsubg  24005  tsmsres  24038  icccmplem2  24719  uniioombllem4  25494  ppiprm  27068  chtprm  27070  pntrsumbnd2  27485  noextend  27585  nodenselem5  27607  nosupbnd2lem1  27634  addsproplem1  27883  addsprop  27890  negsproplem1  27941  negsprop  27948  mulsproplemcbv  28025  mulsproplem1  28026  mulsprop  28040  precsexlemcbv  28115  precsexlem3  28118  onsleft  28168  sltonold  28169  onscutlt  28172  pthdlem1  29703  wwlksnext  29830  clwwlknonex2lem1  30043  iunxunsn  32502  iunxunpr  32503  difres  32536  ofpreima2  32597  fzspl  32719  tocyc01  33082  ordtprsuni  33916  ordtcnvNEW  33917  carsgsigalem  34313  ballotlemfp1  34490  fsum2dsub  34605  reprsuc  34613  bnj941  34769  bnj944  34935  fineqvac  35094  subfacp1lem1  35173  cvmscld  35267  satf  35347  satfv1  35357  fmlasuc  35380  mrsubvrs  35516  mclsval  35557  rankaltopb  35974  rankung  36161  lindsadd  37614  lindsenlbs  37616  poimirlem1  37622  poimirlem2  37623  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem13  37634  poimirlem14  37635  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem26  37647  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  lshpnel2N  38985  paddfval  39798  hdmapval  41829  fzsplitnd  41977  lcmfunnnd  42007  fsuppssind  42588  diophren  42808  omabs2  43328  tfsconcatrn  43338  tfsconcatrev  43344  iunrelexp0  43698  trclfvdecoml  43725  isotone1  44044  iunp1  45067  snunioo1  45517  dvmptfprodlem  45949  stoweidlem11  46016  stoweidlem26  46031  fourierdlem33  46145  fzopredsuc  47328  iccpartltu  47430  iccpartgt  47432  dfclnbgr2  47828  dfclnbgr4  47829  dfclnbgr3  47831  clnbupgr  47838  clnbgr0edg  47841  dfclnbgr5  47854  dfclnbgr6  47860  dfsclnbgr6  47862  cycl3grtri  47950  stgrclnbgr0  47968  lmod1zr  48486  tposres2  48872