Theorem uneq2d 4121

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

Syntax hints:   → wi 4   = wceq 1560   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  ifeq2  4485  tpeq3  4703  iununi  5056  sucprc  6424  unisucs  6425  resasplit  6734  fvun1  6958  fmptapd  7155  fndifnfp  7160  fvunsn  7163  fnsnsplit  7168  f1ofvswap  7290  oev2  8492  oarec  8531  ralxpmap  8878  sbthlem5  9063  sbthlem6  9064  domss2  9108  dif1en  9130  unfi  9139  fodomfi  9256  domunfican  9266  fiint  9271  pm54.43  9959  kmlem2  10108  kmlem11  10117  ackbij1lem1  10175  fin23lem26  10282  axdc3lem4  10410  fpwwe2lem12  10600  wunex2  10696  wuncval2  10705  indconst1  12208  ioounsn  13481  snunico  13483  ioojoin  13487  fzsuc  13576  fseq1p1m1  13603  fseq1m1p1  13604  fzosplitsnm1  13746  fzosplitsn  13782  fzosplitpr  13783  fzosplitprm1  13784  hashfun  14450  resunimafz0  14458  s4prop  14923  fsumm1  15778  climcndslem1  15879  fprodm1  15997  ruclem4  16266  lcmfunsnlem1  16671  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  lcmfunsn  16678  vdwap1  17013  setscom  17216  setsidvald  17235  mreexmrid  17675  mreexexlemd  17676  mreexexlem2d  17677  cnvtsr  18620  dprd2da  20084  dmdprdsplit2lem  20087  lspun0  21078  lbsextlem4  21231  cmpcld  23462  comppfsc  23592  trfil2  23947  cldsubg  24171  tsmsres  24204  icccmplem2  24884  uniioombllem4  25648  ppiprm  27215  chtprm  27217  pntrsumbnd2  27631  noextend  27730  nodenselem5  27752  nosupbnd2lem1  27779  addsproplem1  28062  addsprop  28069  negsproplem1  28121  negsprop  28128  mulsproplemcbv  28208  mulsproplem1  28209  mulsprop  28223  precsexlemcbv  28299  precsexlem3  28302  onleft  28353  ltonold  28354  oncutlt  28357  pthdlem1  29966  wwlksnext  30093  clwwlknonex2lem1  30309  iunxunsn  32766  iunxunpr  32767  difres  32800  ofpreima2  32868  fzspl  32991  tocyc01  33298  esplyind  33872  ordtprsuni  34216  ordtcnvNEW  34217  carsgsigalem  34612  ballotlemfp1  34789  fsum2dsub  34901  reprsuc  34909  bnj941  35068  bnj944  35233  fineqvac  35412  subfacp1lem1  35529  cvmscld  35623  satf  35703  satfv1  35713  fmlasuc  35736  mrsubvrs  35872  mclsval  35913  rankaltopb  36329  rankung  36516  lindsadd  38112  lindsenlbs  38114  poimirlem1  38120  poimirlem2  38121  poimirlem4  38123  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  poimirlem13  38132  poimirlem14  38133  poimirlem16  38135  poimirlem17  38136  poimirlem18  38137  poimirlem19  38138  poimirlem20  38139  poimirlem21  38140  poimirlem22  38141  poimirlem26  38145  poimirlem28  38147  poimirlem31  38150  poimirlem32  38151  lshpnel2N  39609  paddfval  40421  hdmapval  42452  fzsplitnd  42599  lcmfunnnd  42629  fsuppssind  43175  diophren  43390  omabs2  43909  tfsconcatrn  43919  tfsconcatrev  43925  iunrelexp0  44278  trclfvdecoml  44305  isotone1  44624  iunp1  45646  snunioo1  46088  dvmptfprodlem  46518  stoweidlem11  46585  stoweidlem26  46600  fourierdlem33  46714  fzopredsuc  47918  iccpartltu  48031  iccpartgt  48033  dfclnbgr2  48445  dfclnbgr4  48446  dfclnbgr3  48448  clnbupgr  48455  clnbgr0edg  48459  dfclnbgr5  48472  dfclnbgr6  48478  dfsclnbgr6  48480  cycl3grtri  48569  stgrclnbgr0  48587  lmod1zr  49115  tposres2  49501