Theorem uneq2d 4177

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

Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  ifeq2  4535  tpeq3  4748  iununi  5103  sucprc  6461  unisucs  6462  resasplit  6778  fvun1  6999  fmptapd  7190  fndifnfp  7195  fvunsn  7198  fnsnsplit  7203  f1ofvswap  7325  oev2  8559  oarec  8598  ralxpmap  8934  sbthlem5  9125  sbthlem6  9126  domss2  9174  dif1en  9198  dif1enOLD  9200  unfi  9209  fodomfi  9347  domunfican  9358  fiint  9363  fiintOLD  9364  fodomfiOLD  9367  pm54.43  10038  kmlem2  10189  kmlem11  10198  ackbij1lem1  10256  fin23lem26  10362  axdc3lem4  10490  fpwwe2lem12  10679  wunex2  10775  wuncval2  10784  ioounsn  13513  snunico  13515  ioojoin  13519  fzsuc  13607  fseq1p1m1  13634  fseq1m1p1  13635  fzosplitsnm1  13775  fzosplitsn  13810  fzosplitpr  13811  fzosplitprm1  13812  hashfun  14472  resunimafz0  14480  s4prop  14945  fsumm1  15783  climcndslem1  15881  fprodm1  15999  ruclem4  16266  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfunsn  16677  vdwap1  17010  setscom  17213  setsidvald  17232  setsidvaldOLD  17233  mreexmrid  17687  mreexexlemd  17688  mreexexlem2d  17689  cnvtsr  18645  dprd2da  20076  dmdprdsplit2lem  20079  lspun0  21026  lbsextlem4  21180  cmpcld  23425  comppfsc  23555  trfil2  23910  cldsubg  24134  tsmsres  24167  icccmplem2  24858  uniioombllem4  25634  ppiprm  27208  chtprm  27210  pntrsumbnd2  27625  noextend  27725  nodenselem5  27747  nosupbnd2lem1  27774  addsproplem1  28016  addsprop  28023  negsproplem1  28074  negsprop  28081  mulsproplemcbv  28155  mulsproplem1  28156  mulsprop  28170  precsexlemcbv  28244  precsexlem3  28247  sltonold  28297  pthdlem1  29798  wwlksnext  29922  clwwlknonex2lem1  30135  iunxunsn  32586  iunxunpr  32587  difres  32619  ofpreima2  32682  fzspl  32797  tocyc01  33120  ordtprsuni  33879  ordtcnvNEW  33880  carsgsigalem  34296  ballotlemfp1  34472  fsum2dsub  34600  reprsuc  34608  bnj941  34764  bnj944  34930  fineqvac  35089  subfacp1lem1  35163  cvmscld  35257  satf  35337  satfv1  35347  fmlasuc  35370  mrsubvrs  35506  mclsval  35547  rankaltopb  35960  rankung  36147  lindsadd  37599  lindsenlbs  37601  poimirlem1  37607  poimirlem2  37608  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem26  37632  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  lshpnel2N  38966  paddfval  39779  hdmapval  41810  fzsplitnd  41963  lcmfunnnd  41993  metakunt24  42209  fsuppssind  42579  diophren  42800  omabs2  43321  tfsconcatrn  43331  tfsconcatrev  43337  iunrelexp0  43691  trclfvdecoml  43718  isotone1  44037  iunp1  45005  snunioo1  45464  dvmptfprodlem  45899  stoweidlem11  45966  stoweidlem26  45981  fourierdlem33  46095  fzopredsuc  47272  iccpartltu  47349  iccpartgt  47351  dfclnbgr2  47747  dfclnbgr4  47748  dfclnbgr3  47750  clnbupgr  47757  clnbgr0edg  47760  dfclnbgr5  47773  dfclnbgr6  47779  dfsclnbgr6  47781  stgrclnbgr0  47867  lmod1zr  48338