Theorem uneq2d 4090

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

Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  ifeq2  4430  tpeq3  4640  iununi  4984  sucprc  6234  resasplit  6522  fvun1  6729  fmptapd  6910  fndifnfp  6915  fvunsn  6918  fnsnsplit  6923  oev2  8131  oarec  8171  ralxpmap  8443  sbthlem5  8615  sbthlem6  8616  domss2  8660  domunfican  8775  fiint  8779  fodomfi  8781  pm54.43  9414  kmlem2  9562  kmlem11  9571  ackbij1lem1  9631  fin23lem26  9736  axdc3lem4  9864  fpwwe2lem13  10053  wunex2  10149  wuncval2  10158  ioounsn  12855  snunico  12857  ioojoin  12861  fzsuc  12949  fseq1p1m1  12976  fseq1m1p1  12977  fzosplitsnm1  13107  fzosplitsn  13140  fzosplitpr  13141  fzosplitprm1  13142  hashfun  13794  resunimafz0  13799  s4prop  14263  fsumm1  15098  climcndslem1  15196  fprodm1  15313  ruclem4  15579  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  lcmfunsn  15978  vdwap1  16303  setsidvald  16506  setscom  16519  mreexmrid  16906  mreexexlemd  16907  mreexexlem2d  16908  cnvtsr  17824  dprd2da  19157  dmdprdsplit2lem  19160  lspun0  19776  lbsextlem4  19926  cmpcld  22007  comppfsc  22137  trfil2  22492  cldsubg  22716  tsmsres  22749  icccmplem2  23428  uniioombllem4  24190  ppiprm  25736  chtprm  25738  pntrsumbnd2  26151  pthdlem1  27555  wwlksnext  27679  clwwlknonex2lem1  27892  iunxunsn  30330  iunxunpr  30331  difres  30363  ofpreima2  30429  fzspl  30539  tocyc01  30810  ordtprsuni  31272  ordtcnvNEW  31273  carsgsigalem  31683  ballotlemfp1  31859  fsum2dsub  31988  reprsuc  31996  bnj941  32154  bnj944  32320  subfacp1lem1  32539  cvmscld  32633  satf  32713  satfv1  32723  fmlasuc  32746  mrsubvrs  32882  mclsval  32923  noextend  33286  nodenselem5  33305  nosupbnd2lem1  33328  rankaltopb  33553  rankung  33740  lindsadd  35050  lindsenlbs  35052  poimirlem1  35058  poimirlem2  35059  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem13  35070  poimirlem14  35071  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem26  35083  poimirlem28  35085  poimirlem31  35088  poimirlem32  35089  lshpnel2N  36281  paddfval  37093  hdmapval  39124  fzsplitnd  39270  lcmfunnnd  39300  metakunt24  39373  fsuppssind  39459  diophren  39754  iunrelexp0  40403  trclfvdecoml  40430  isotone1  40751  iunp1  41700  snunioo1  42149  dvmptfprodlem  42586  stoweidlem11  42653  stoweidlem26  42668  fourierdlem33  42782  fzopredsuc  43880  iccpartltu  43942  iccpartgt  43944  lmod1zr  44902