Theorem uneq2d 4113

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  ifeq2  4475  tpeq3  4692  iununi  5042  sucprc  6379  unisucs  6380  resasplit  6688  fvun1  6908  fmptapd  7100  fndifnfp  7105  fvunsn  7108  fnsnsplit  7113  f1ofvswap  7235  oev2  8433  oarec  8472  ralxpmap  8815  sbthlem5  8999  sbthlem6  9000  domss2  9044  dif1en  9066  unfi  9075  fodomfi  9191  domunfican  9201  fiint  9206  fodomfiOLD  9209  pm54.43  9889  kmlem2  10038  kmlem11  10047  ackbij1lem1  10105  fin23lem26  10211  axdc3lem4  10339  fpwwe2lem12  10528  wunex2  10624  wuncval2  10633  ioounsn  13372  snunico  13374  ioojoin  13378  fzsuc  13466  fseq1p1m1  13493  fseq1m1p1  13494  fzosplitsnm1  13635  fzosplitsn  13671  fzosplitpr  13672  fzosplitprm1  13673  hashfun  14339  resunimafz0  14347  s4prop  14812  fsumm1  15653  climcndslem1  15751  fprodm1  15869  ruclem4  16138  lcmfunsnlem1  16543  lcmfunsnlem2lem1  16544  lcmfunsnlem2lem2  16545  lcmfunsnlem2  16546  lcmfunsn  16550  vdwap1  16884  setscom  17086  setsidvald  17105  mreexmrid  17544  mreexexlemd  17545  mreexexlem2d  17546  cnvtsr  18489  dprd2da  19951  dmdprdsplit2lem  19954  lspun0  20939  lbsextlem4  21093  cmpcld  23312  comppfsc  23442  trfil2  23797  cldsubg  24021  tsmsres  24054  icccmplem2  24734  uniioombllem4  25509  ppiprm  27083  chtprm  27085  pntrsumbnd2  27500  noextend  27600  nodenselem5  27622  nosupbnd2lem1  27649  addsproplem1  27907  addsprop  27914  negsproplem1  27965  negsprop  27972  mulsproplemcbv  28049  mulsproplem1  28050  mulsprop  28064  precsexlemcbv  28139  precsexlem3  28142  onsleft  28192  sltonold  28193  onscutlt  28196  pthdlem1  29739  wwlksnext  29866  clwwlknonex2lem1  30079  iunxunsn  32538  iunxunpr  32539  difres  32572  ofpreima2  32640  fzspl  32764  tocyc01  33079  ordtprsuni  33924  ordtcnvNEW  33925  carsgsigalem  34320  ballotlemfp1  34497  fsum2dsub  34612  reprsuc  34620  bnj941  34776  bnj944  34942  fineqvac  35131  subfacp1lem1  35215  cvmscld  35309  satf  35389  satfv1  35399  fmlasuc  35422  mrsubvrs  35558  mclsval  35599  rankaltopb  36013  rankung  36200  lindsadd  37653  lindsenlbs  37655  poimirlem1  37661  poimirlem2  37662  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem8  37668  poimirlem13  37673  poimirlem14  37674  poimirlem16  37676  poimirlem17  37677  poimirlem18  37678  poimirlem19  37679  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem26  37686  poimirlem28  37688  poimirlem31  37691  poimirlem32  37692  lshpnel2N  39024  paddfval  39836  hdmapval  41867  fzsplitnd  42015  lcmfunnnd  42045  fsuppssind  42626  diophren  42846  omabs2  43365  tfsconcatrn  43375  tfsconcatrev  43381  iunrelexp0  43735  trclfvdecoml  43762  isotone1  44081  iunp1  45103  snunioo1  45552  dvmptfprodlem  45982  stoweidlem11  46049  stoweidlem26  46064  fourierdlem33  46178  fzopredsuc  47354  iccpartltu  47456  iccpartgt  47458  dfclnbgr2  47854  dfclnbgr4  47855  dfclnbgr3  47857  clnbupgr  47864  clnbgr0edg  47868  dfclnbgr5  47881  dfclnbgr6  47887  dfsclnbgr6  47889  cycl3grtri  47978  stgrclnbgr0  47996  lmod1zr  48525  tposres2  48911