Theorem uneq2d 4170

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  ifeq2  4490  tpeq3  4707  iununi  5064  sucprc  6467  unisucs  6468  resasplit  6782  fvun1  7007  fmptapd  7207  fndifnfp  7212  fvunsn  7215  fnsnsplit  7220  f1ofvswap  7345  oev2  8569  oarec  8608  ralxpmap  8962  sbthlem5  9148  sbthlem6  9149  domss2  9193  dif1en  9215  unfi  9224  fodomfi  9342  domunfican  9351  fiint  9356  rankung  9910  pm54.43  10121  kmlem2  10269  kmlem11  10278  ackbij1lem1  10336  fin23lem26  10442  axdc3lem4  10570  fpwwe2lem12  10766  wunex2  10862  wuncval2  10871  indconst1  12373  ioounsn  13648  snunico  13650  ioojoin  13654  fzsuc  13745  fseq1p1m1  13772  fseq1m1p1  13773  fzosplitsnm1  13915  fzosplitsn  13951  fzosplitpr  13952  fzosplitprm1  13953  hashfun  14623  resunimafz0  14631  s4prop  15104  fsumm1  15961  climcndslem1  16062  fprodm1  16178  ruclem4  16446  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfunsn  16863  vdwap1  17199  setscom  17402  setsidvald  17421  mreexmrid  17867  mreexexlemd  17868  mreexexlem2d  17869  cnvtsr  18812  dprd2da  20309  dmdprdsplit2lem  20312  lspun0  21337  lbsextlem4  21490  lindsenlbs  22212  cmpcld  23775  comppfsc  23906  trfil2  24261  cldsubg  24485  tsmsres  24518  icccmplem2  25198  uniioombllem4  25962  ppiprm  27535  chtprm  27537  pntrsumbnd2  27951  noextend  28080  nodenselem5  28102  nosupbnd2lem1  28129  addsproplem1  28412  addsprop  28419  negsproplem1  28471  negsprop  28478  mulsproplemcbv  28558  mulsproplem1  28559  mulsprop  28573  precsexlemcbv  28649  precsexlem3  28652  onleft  28703  ltonold  28704  oncutlt  28707  pthdlem1  30409  wwlksnext  30539  clwwlknonex2lem1  30755  iunxunsn  33258  iunxunpr  33259  difres  33292  ofpreima2  33358  fzspl  33477  tocyc01  33778  esplyind  34318  ordtprsuni  34662  ordtcnvNEW  34663  carsgsigalem  35058  ballotlemfp1  35235  fsum2dsub  35347  reprsuc  35355  bnj941  35514  bnj944  35679  fineqvac  35925  subfacp1lem1  36152  cvmscld  36246  satf  36326  satfv1  36336  fmlasuc  36359  mrsubvrs  36495  mclsval  36536  rankaltopb  36959  lindsadd  38804  poimirlem1  38807  poimirlem2  38808  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem26  38832  poimirlem28  38834  poimirlem31  38837  poimirlem32  38838  lshpnel2N  40308  paddfval  41120  hdmapval  43151  fzsplitnd  43298  lcmfunnnd  43328  fsuppssind  43887  diophren  44086  omabs2  44595  tfsconcatrn  44605  tfsconcatrev  44611  iunrelexp0  44963  trclfvdecoml  44990  isotone1  45309  iunp1  46357  snunioo1  46797  dvmptfprodlem  47227  stoweidlem11  47294  stoweidlem26  47309  fourierdlem33  47423  fzopredsuc  48667  iccpartltu  48780  iccpartgt  48782  dfclnbgr2  49194  dfclnbgr4  49195  dfclnbgr3  49197  clnbupgr  49204  clnbgr0edg  49208  dfclnbgr5  49221  dfclnbgr6  49227  dfsclnbgr6  49229  cycl3grtri  49318  stgrclnbgr0  49336  azval  49716  lmod1zr  49936  tposres2  50324