Theorem uneq2d 4130

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

Syntax hints:   → wi 4   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  ifeq2  4497  tpeq3  4715  iununi  5069  sucprc  6440  unisucs  6441  resasplit  6749  fvun1  6973  fmptapd  7170  fndifnfp  7175  fvunsn  7178  fnsnsplit  7183  f1ofvswap  7305  oev2  8508  oarec  8547  ralxpmap  8894  sbthlem5  9079  sbthlem6  9080  domss2  9124  dif1en  9146  unfi  9155  fodomfi  9272  domunfican  9281  fiint  9286  pm54.43  9987  kmlem2  10135  kmlem11  10144  ackbij1lem1  10202  fin23lem26  10309  axdc3lem4  10437  fpwwe2lem12  10627  wunex2  10723  wuncval2  10732  indconst1  12231  ioounsn  13504  snunico  13506  ioojoin  13510  fzsuc  13599  fseq1p1m1  13626  fseq1m1p1  13627  fzosplitsnm1  13769  fzosplitsn  13805  fzosplitpr  13806  fzosplitprm1  13807  hashfun  14474  resunimafz0  14482  s4prop  14947  fsumm1  15802  climcndslem1  15903  fprodm1  16021  ruclem4  16290  lcmfunsnlem1  16695  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  lcmfunsnlem2  16698  lcmfunsn  16702  vdwap1  17037  setscom  17240  setsidvald  17259  mreexmrid  17699  mreexexlemd  17700  mreexexlem2d  17701  cnvtsr  18644  dprd2da  20114  dmdprdsplit2lem  20117  lspun0  21110  lbsextlem4  21263  cmpcld  23528  comppfsc  23658  trfil2  24013  cldsubg  24237  tsmsres  24270  icccmplem2  24950  uniioombllem4  25714  ppiprm  27281  chtprm  27283  pntrsumbnd2  27697  noextend  27796  nodenselem5  27818  nosupbnd2lem1  27845  addsproplem1  28128  addsprop  28135  negsproplem1  28187  negsprop  28194  mulsproplemcbv  28274  mulsproplem1  28275  mulsprop  28289  precsexlemcbv  28365  precsexlem3  28368  onleft  28419  ltonold  28420  oncutlt  28423  pthdlem1  30056  wwlksnext  30183  clwwlknonex2lem1  30399  iunxunsn  32852  iunxunpr  32853  difres  32886  ofpreima2  32952  fzspl  33075  tocyc01  33379  esplyind  33910  ordtprsuni  34254  ordtcnvNEW  34255  carsgsigalem  34650  ballotlemfp1  34827  fsum2dsub  34939  reprsuc  34947  bnj941  35106  bnj944  35271  fineqvac  35452  subfacp1lem1  35570  cvmscld  35664  satf  35744  satfv1  35754  fmlasuc  35777  mrsubvrs  35913  mclsval  35954  rankaltopb  36370  rankung  36557  lindsadd  38152  lindsenlbs  38154  poimirlem1  38160  poimirlem2  38161  poimirlem4  38163  poimirlem6  38165  poimirlem7  38166  poimirlem8  38167  poimirlem13  38172  poimirlem14  38173  poimirlem16  38175  poimirlem17  38176  poimirlem18  38177  poimirlem19  38178  poimirlem20  38179  poimirlem21  38180  poimirlem22  38181  poimirlem26  38185  poimirlem28  38187  poimirlem31  38190  poimirlem32  38191  lshpnel2N  39649  paddfval  40461  hdmapval  42492  fzsplitnd  42639  lcmfunnnd  42669  fsuppssind  43217  diophren  43432  omabs2  43951  tfsconcatrn  43961  tfsconcatrev  43967  iunrelexp0  44320  trclfvdecoml  44347  isotone1  44666  iunp1  45678  snunioo1  46120  dvmptfprodlem  46550  stoweidlem11  46617  stoweidlem26  46632  fourierdlem33  46746  fzopredsuc  47950  iccpartltu  48063  iccpartgt  48065  dfclnbgr2  48477  dfclnbgr4  48478  dfclnbgr3  48480  clnbupgr  48487  clnbgr0edg  48491  dfclnbgr5  48504  dfclnbgr6  48510  dfsclnbgr6  48512  cycl3grtri  48601  stgrclnbgr0  48619  lmod1zr  49158  tposres2  49543