Theorem uneq2d 4115

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  ifeq2  4487  tpeq3  4705  iununi  5059  sucprc  6441  unisucs  6442  resasplit  6752  fvun1  6976  fmptapd  7176  fndifnfp  7181  fvunsn  7184  fnsnsplit  7189  f1ofvswap  7314  oev2  8531  oarec  8570  ralxpmap  8924  sbthlem5  9110  sbthlem6  9111  domss2  9155  dif1en  9177  unfi  9186  fodomfi  9304  domunfican  9313  fiint  9318  rankung  9873  pm54.43  10082  kmlem2  10230  kmlem11  10239  ackbij1lem1  10297  fin23lem26  10403  axdc3lem4  10531  fpwwe2lem12  10727  wunex2  10823  wuncval2  10832  indconst1  12333  ioounsn  13608  snunico  13610  ioojoin  13614  fzsuc  13705  fseq1p1m1  13732  fseq1m1p1  13733  fzosplitsnm1  13875  fzosplitsn  13911  fzosplitpr  13912  fzosplitprm1  13913  hashfun  14582  resunimafz0  14590  s4prop  15061  fsumm1  15917  climcndslem1  16018  fprodm1  16134  ruclem4  16402  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  lcmfunsn  16819  vdwap1  17155  setscom  17358  setsidvald  17377  mreexmrid  17817  mreexexlemd  17818  mreexexlem2d  17819  cnvtsr  18762  dprd2da  20258  dmdprdsplit2lem  20261  lspun0  21286  lbsextlem4  21439  lindsenlbs  22157  cmpcld  23720  comppfsc  23851  trfil2  24206  cldsubg  24430  tsmsres  24463  icccmplem2  25143  uniioombllem4  25907  ppiprm  27478  chtprm  27480  pntrsumbnd2  27894  noextend  28023  nodenselem5  28045  nosupbnd2lem1  28072  addsproplem1  28355  addsprop  28362  negsproplem1  28414  negsprop  28421  mulsproplemcbv  28501  mulsproplem1  28502  mulsprop  28516  precsexlemcbv  28592  precsexlem3  28595  onleft  28646  ltonold  28647  oncutlt  28650  pthdlem1  30352  wwlksnext  30482  clwwlknonex2lem1  30698  iunxunsn  33160  iunxunpr  33161  difres  33194  ofpreima2  33260  fzspl  33381  tocyc01  33679  esplyind  34207  ordtprsuni  34551  ordtcnvNEW  34552  carsgsigalem  34947  ballotlemfp1  35124  fsum2dsub  35236  reprsuc  35244  bnj941  35403  bnj944  35568  fineqvac  35784  subfacp1lem1  35944  cvmscld  36038  satf  36118  satfv1  36128  fmlasuc  36151  mrsubvrs  36287  mclsval  36328  rankaltopb  36744  lindsadd  38536  poimirlem1  38539  poimirlem2  38540  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem13  38551  poimirlem14  38552  poimirlem16  38554  poimirlem17  38555  poimirlem18  38556  poimirlem19  38557  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem26  38564  poimirlem28  38566  poimirlem31  38569  poimirlem32  38570  lshpnel2N  40042  paddfval  40854  hdmapval  42885  fzsplitnd  43032  lcmfunnnd  43062  fsuppssind  43621  diophren  43819  omabs2  44333  tfsconcatrn  44343  tfsconcatrev  44349  iunrelexp0  44701  trclfvdecoml  44728  isotone1  45047  iunp1  46082  snunioo1  46523  dvmptfprodlem  46953  stoweidlem11  47020  stoweidlem26  47035  fourierdlem33  47149  fzopredsuc  48393  iccpartltu  48506  iccpartgt  48508  dfclnbgr2  48920  dfclnbgr4  48921  dfclnbgr3  48923  clnbupgr  48930  clnbgr0edg  48934  dfclnbgr5  48947  dfclnbgr6  48953  dfsclnbgr6  48955  cycl3grtri  49044  stgrclnbgr0  49062  lmod1zr  49604  tposres2  49987