Theorem uneq2d 4191

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  ifeq2  4553  tpeq3  4769  iununi  5122  sucprc  6471  unisucs  6472  resasplit  6791  fvun1  7013  fmptapd  7205  fndifnfp  7210  fvunsn  7213  fnsnsplit  7218  f1ofvswap  7342  oev2  8579  oarec  8618  ralxpmap  8954  sbthlem5  9153  sbthlem6  9154  domss2  9202  dif1en  9226  dif1enOLD  9228  unfi  9238  fodomfi  9378  domunfican  9389  fiint  9394  fiintOLD  9395  fodomfiOLD  9398  pm54.43  10070  kmlem2  10221  kmlem11  10230  ackbij1lem1  10288  fin23lem26  10394  axdc3lem4  10522  fpwwe2lem12  10711  wunex2  10807  wuncval2  10816  ioounsn  13537  snunico  13539  ioojoin  13543  fzsuc  13631  fseq1p1m1  13658  fseq1m1p1  13659  fzosplitsnm1  13791  fzosplitsn  13825  fzosplitpr  13826  fzosplitprm1  13827  hashfun  14486  resunimafz0  14494  s4prop  14959  fsumm1  15799  climcndslem1  15897  fprodm1  16015  ruclem4  16282  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  lcmfunsn  16691  vdwap1  17024  setscom  17227  setsidvald  17246  setsidvaldOLD  17247  mreexmrid  17701  mreexexlemd  17702  mreexexlem2d  17703  cnvtsr  18658  dprd2da  20086  dmdprdsplit2lem  20089  lspun0  21032  lbsextlem4  21186  cmpcld  23431  comppfsc  23561  trfil2  23916  cldsubg  24140  tsmsres  24173  icccmplem2  24864  uniioombllem4  25640  ppiprm  27212  chtprm  27214  pntrsumbnd2  27629  noextend  27729  nodenselem5  27751  nosupbnd2lem1  27778  addsproplem1  28020  addsprop  28027  negsproplem1  28078  negsprop  28085  mulsproplemcbv  28159  mulsproplem1  28160  mulsprop  28174  precsexlemcbv  28248  precsexlem3  28251  sltonold  28301  pthdlem1  29802  wwlksnext  29926  clwwlknonex2lem1  30139  iunxunsn  32589  iunxunpr  32590  difres  32622  ofpreima2  32684  fzspl  32795  tocyc01  33111  ordtprsuni  33865  ordtcnvNEW  33866  carsgsigalem  34280  ballotlemfp1  34456  fsum2dsub  34584  reprsuc  34592  bnj941  34748  bnj944  34914  fineqvac  35073  subfacp1lem1  35147  cvmscld  35241  satf  35321  satfv1  35331  fmlasuc  35354  mrsubvrs  35490  mclsval  35531  rankaltopb  35943  rankung  36130  lindsadd  37573  lindsenlbs  37575  poimirlem1  37581  poimirlem2  37582  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem26  37606  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  lshpnel2N  38941  paddfval  39754  hdmapval  41785  fzsplitnd  41939  lcmfunnnd  41969  metakunt24  42185  fsuppssind  42548  diophren  42769  omabs2  43294  tfsconcatrn  43304  tfsconcatrev  43310  iunrelexp0  43664  trclfvdecoml  43691  isotone1  44010  iunp1  44968  snunioo1  45430  dvmptfprodlem  45865  stoweidlem11  45932  stoweidlem26  45947  fourierdlem33  46061  fzopredsuc  47238  iccpartltu  47299  iccpartgt  47301  dfclnbgr2  47697  dfclnbgr4  47698  dfclnbgr3  47699  clnbupgr  47706  clnbgr0edg  47709  dfclnbgr5  47722  dfclnbgr6  47728  dfsclnbgr6  47730  lmod1zr  48222