Theorem uneq2d 4122

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

Syntax hints:   → wi 4   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  ifeq2  4492  tpeq3  4710  iununi  5065  sucprc  6439  unisucs  6440  resasplit  6748  fvun1  6972  fmptapd  7169  fndifnfp  7174  fvunsn  7177  fnsnsplit  7182  f1ofvswap  7304  oev2  8504  oarec  8543  ralxpmap  8890  sbthlem5  9075  sbthlem6  9076  domss2  9120  dif1en  9142  unfi  9151  fodomfi  9268  domunfican  9277  fiint  9282  pm54.43  9983  kmlem2  10131  kmlem11  10140  ackbij1lem1  10198  fin23lem26  10304  axdc3lem4  10432  fpwwe2lem12  10622  wunex2  10718  wuncval2  10727  indconst1  12226  ioounsn  13499  snunico  13501  ioojoin  13505  fzsuc  13595  fseq1p1m1  13622  fseq1m1p1  13623  fzosplitsnm1  13765  fzosplitsn  13801  fzosplitpr  13802  fzosplitprm1  13803  hashfun  14470  resunimafz0  14478  s4prop  14943  fsumm1  15798  climcndslem1  15899  fprodm1  16017  ruclem4  16285  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  lcmfunsn  16697  vdwap1  17032  setscom  17235  setsidvald  17254  mreexmrid  17694  mreexexlemd  17695  mreexexlem2d  17696  cnvtsr  18639  dprd2da  20109  dmdprdsplit2lem  20112  lspun0  21132  lbsextlem4  21285  cmpcld  23559  comppfsc  23689  trfil2  24044  cldsubg  24268  tsmsres  24301  icccmplem2  24981  uniioombllem4  25745  ppiprm  27315  chtprm  27317  pntrsumbnd2  27731  noextend  27830  nodenselem5  27852  nosupbnd2lem1  27879  addsproplem1  28162  addsprop  28169  negsproplem1  28221  negsprop  28228  mulsproplemcbv  28308  mulsproplem1  28309  mulsprop  28323  precsexlemcbv  28399  precsexlem3  28402  onleft  28453  ltonold  28454  oncutlt  28457  pthdlem1  30115  wwlksnext  30242  clwwlknonex2lem1  30458  iunxunsn  32911  iunxunpr  32912  difres  32945  ofpreima2  33011  fzspl  33134  tocyc01  33438  esplyind  33965  ordtprsuni  34309  ordtcnvNEW  34310  carsgsigalem  34705  ballotlemfp1  34882  fsum2dsub  34994  reprsuc  35002  bnj941  35161  bnj944  35326  fineqvac  35529  subfacp1lem1  35671  cvmscld  35765  satf  35845  satfv1  35855  fmlasuc  35878  mrsubvrs  36014  mclsval  36055  rankaltopb  36471  rankung  36658  lindsadd  38284  lindsenlbs  38286  poimirlem1  38292  poimirlem2  38293  poimirlem4  38295  poimirlem6  38297  poimirlem7  38298  poimirlem8  38299  poimirlem13  38304  poimirlem14  38305  poimirlem16  38307  poimirlem17  38308  poimirlem18  38309  poimirlem19  38310  poimirlem20  38311  poimirlem21  38312  poimirlem22  38313  poimirlem26  38317  poimirlem28  38319  poimirlem31  38322  poimirlem32  38323  lshpnel2N  39779  paddfval  40591  hdmapval  42622  fzsplitnd  42769  lcmfunnnd  42799  fsuppssind  43345  diophren  43560  omabs2  44079  tfsconcatrn  44089  tfsconcatrev  44095  iunrelexp0  44448  trclfvdecoml  44475  isotone1  44794  iunp1  45806  snunioo1  46248  dvmptfprodlem  46678  stoweidlem11  46745  stoweidlem26  46760  fourierdlem33  46874  fzopredsuc  48081  iccpartltu  48194  iccpartgt  48196  dfclnbgr2  48608  dfclnbgr4  48609  dfclnbgr3  48611  clnbupgr  48618  clnbgr0edg  48622  dfclnbgr5  48635  dfclnbgr6  48641  dfsclnbgr6  48643  cycl3grtri  48732  stgrclnbgr0  48750  lmod1zr  49293  tposres2  49678