Theorem uneq2d 4120

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  ifeq2  4484  tpeq3  4701  iununi  5054  sucprc  6395  unisucs  6396  resasplit  6704  fvun1  6925  fmptapd  7117  fndifnfp  7122  fvunsn  7125  fnsnsplit  7130  f1ofvswap  7252  oev2  8450  oarec  8489  ralxpmap  8834  sbthlem5  9019  sbthlem6  9020  domss2  9064  dif1en  9086  unfi  9095  fodomfi  9212  domunfican  9222  fiint  9227  fodomfiOLD  9230  pm54.43  9913  kmlem2  10062  kmlem11  10071  ackbij1lem1  10129  fin23lem26  10235  axdc3lem4  10363  fpwwe2lem12  10553  wunex2  10649  wuncval2  10658  ioounsn  13393  snunico  13395  ioojoin  13399  fzsuc  13487  fseq1p1m1  13514  fseq1m1p1  13515  fzosplitsnm1  13656  fzosplitsn  13692  fzosplitpr  13693  fzosplitprm1  13694  hashfun  14360  resunimafz0  14368  s4prop  14833  fsumm1  15674  climcndslem1  15772  fprodm1  15890  ruclem4  16159  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfunsn  16571  vdwap1  16905  setscom  17107  setsidvald  17126  mreexmrid  17566  mreexexlemd  17567  mreexexlem2d  17568  cnvtsr  18511  dprd2da  19973  dmdprdsplit2lem  19976  lspun0  20962  lbsextlem4  21116  cmpcld  23346  comppfsc  23476  trfil2  23831  cldsubg  24055  tsmsres  24088  icccmplem2  24768  uniioombllem4  25543  ppiprm  27117  chtprm  27119  pntrsumbnd2  27534  noextend  27634  nodenselem5  27656  nosupbnd2lem1  27683  addsproplem1  27965  addsprop  27972  negsproplem1  28024  negsprop  28031  mulsproplemcbv  28111  mulsproplem1  28112  mulsprop  28126  precsexlemcbv  28202  precsexlem3  28205  onleft  28256  ltonold  28257  oncutlt  28260  pthdlem1  29839  wwlksnext  29966  clwwlknonex2lem1  30182  iunxunsn  32641  iunxunpr  32642  difres  32675  ofpreima2  32744  fzspl  32869  indconst1  32940  tocyc01  33200  esplyind  33731  ordtprsuni  34076  ordtcnvNEW  34077  carsgsigalem  34472  ballotlemfp1  34649  fsum2dsub  34764  reprsuc  34772  bnj941  34928  bnj944  35094  fineqvac  35272  subfacp1lem1  35373  cvmscld  35467  satf  35547  satfv1  35557  fmlasuc  35580  mrsubvrs  35716  mclsval  35757  rankaltopb  36173  rankung  36360  lindsadd  37814  lindsenlbs  37816  poimirlem1  37822  poimirlem2  37823  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem26  37847  poimirlem28  37849  poimirlem31  37852  poimirlem32  37853  lshpnel2N  39245  paddfval  40057  hdmapval  42088  fzsplitnd  42236  lcmfunnnd  42266  fsuppssind  42836  diophren  43055  omabs2  43574  tfsconcatrn  43584  tfsconcatrev  43590  iunrelexp0  43943  trclfvdecoml  43970  isotone1  44289  iunp1  45311  snunioo1  45758  dvmptfprodlem  46188  stoweidlem11  46255  stoweidlem26  46270  fourierdlem33  46384  fzopredsuc  47569  iccpartltu  47671  iccpartgt  47673  dfclnbgr2  48069  dfclnbgr4  48070  dfclnbgr3  48072  clnbupgr  48079  clnbgr0edg  48083  dfclnbgr5  48096  dfclnbgr6  48102  dfsclnbgr6  48104  cycl3grtri  48193  stgrclnbgr0  48211  lmod1zr  48739  tposres2  49125