Theorem uneq2d 4127

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  ifeq2  4489  tpeq3  4704  iununi  5058  sucprc  6398  unisucs  6399  resasplit  6712  fvun1  6934  fmptapd  7127  fndifnfp  7132  fvunsn  7135  fnsnsplit  7140  f1ofvswap  7263  oev2  8464  oarec  8503  ralxpmap  8846  sbthlem5  9032  sbthlem6  9033  domss2  9077  dif1en  9101  dif1enOLD  9103  unfi  9112  fodomfi  9237  domunfican  9248  fiint  9253  fiintOLD  9254  fodomfiOLD  9257  pm54.43  9930  kmlem2  10081  kmlem11  10090  ackbij1lem1  10148  fin23lem26  10254  axdc3lem4  10382  fpwwe2lem12  10571  wunex2  10667  wuncval2  10676  ioounsn  13414  snunico  13416  ioojoin  13420  fzsuc  13508  fseq1p1m1  13535  fseq1m1p1  13536  fzosplitsnm1  13677  fzosplitsn  13712  fzosplitpr  13713  fzosplitprm1  13714  hashfun  14378  resunimafz0  14386  s4prop  14852  fsumm1  15693  climcndslem1  15791  fprodm1  15909  ruclem4  16178  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfunsn  16590  vdwap1  16924  setscom  17126  setsidvald  17145  mreexmrid  17580  mreexexlemd  17581  mreexexlem2d  17582  cnvtsr  18523  dprd2da  19950  dmdprdsplit2lem  19953  lspun0  20893  lbsextlem4  21047  cmpcld  23265  comppfsc  23395  trfil2  23750  cldsubg  23974  tsmsres  24007  icccmplem2  24688  uniioombllem4  25463  ppiprm  27037  chtprm  27039  pntrsumbnd2  27454  noextend  27554  nodenselem5  27576  nosupbnd2lem1  27603  addsproplem1  27852  addsprop  27859  negsproplem1  27910  negsprop  27917  mulsproplemcbv  27994  mulsproplem1  27995  mulsprop  28009  precsexlemcbv  28084  precsexlem3  28087  onsleft  28137  sltonold  28138  onscutlt  28141  pthdlem1  29669  wwlksnext  29796  clwwlknonex2lem1  30009  iunxunsn  32468  iunxunpr  32469  difres  32502  ofpreima2  32563  fzspl  32685  tocyc01  33048  ordtprsuni  33882  ordtcnvNEW  33883  carsgsigalem  34279  ballotlemfp1  34456  fsum2dsub  34571  reprsuc  34579  bnj941  34735  bnj944  34901  fineqvac  35060  subfacp1lem1  35139  cvmscld  35233  satf  35313  satfv1  35323  fmlasuc  35346  mrsubvrs  35482  mclsval  35523  rankaltopb  35940  rankung  36127  lindsadd  37580  lindsenlbs  37582  poimirlem1  37588  poimirlem2  37589  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem13  37600  poimirlem14  37601  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem26  37613  poimirlem28  37615  poimirlem31  37618  poimirlem32  37619  lshpnel2N  38951  paddfval  39764  hdmapval  41795  fzsplitnd  41943  lcmfunnnd  41973  fsuppssind  42554  diophren  42774  omabs2  43294  tfsconcatrn  43304  tfsconcatrev  43310  iunrelexp0  43664  trclfvdecoml  43691  isotone1  44010  iunp1  45033  snunioo1  45483  dvmptfprodlem  45915  stoweidlem11  45982  stoweidlem26  45997  fourierdlem33  46111  fzopredsuc  47297  iccpartltu  47399  iccpartgt  47401  dfclnbgr2  47797  dfclnbgr4  47798  dfclnbgr3  47800  clnbupgr  47807  clnbgr0edg  47810  dfclnbgr5  47823  dfclnbgr6  47829  dfsclnbgr6  47831  cycl3grtri  47919  stgrclnbgr0  47937  lmod1zr  48455  tposres2  48841