Theorem uneq2d 4143

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  ifeq2  4505  tpeq3  4720  iununi  5075  sucprc  6429  unisucs  6430  resasplit  6747  fvun1  6969  fmptapd  7162  fndifnfp  7167  fvunsn  7170  fnsnsplit  7175  f1ofvswap  7298  oev2  8533  oarec  8572  ralxpmap  8908  sbthlem5  9099  sbthlem6  9100  domss2  9148  dif1en  9172  dif1enOLD  9174  unfi  9183  fodomfi  9320  domunfican  9331  fiint  9336  fiintOLD  9337  fodomfiOLD  9340  pm54.43  10013  kmlem2  10164  kmlem11  10173  ackbij1lem1  10231  fin23lem26  10337  axdc3lem4  10465  fpwwe2lem12  10654  wunex2  10750  wuncval2  10759  ioounsn  13492  snunico  13494  ioojoin  13498  fzsuc  13586  fseq1p1m1  13613  fseq1m1p1  13614  fzosplitsnm1  13754  fzosplitsn  13789  fzosplitpr  13790  fzosplitprm1  13791  hashfun  14453  resunimafz0  14461  s4prop  14927  fsumm1  15765  climcndslem1  15863  fprodm1  15981  ruclem4  16250  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  lcmfunsn  16661  vdwap1  16995  setscom  17197  setsidvald  17216  mreexmrid  17653  mreexexlemd  17654  mreexexlem2d  17655  cnvtsr  18596  dprd2da  20023  dmdprdsplit2lem  20026  lspun0  20966  lbsextlem4  21120  cmpcld  23338  comppfsc  23468  trfil2  23823  cldsubg  24047  tsmsres  24080  icccmplem2  24761  uniioombllem4  25537  ppiprm  27111  chtprm  27113  pntrsumbnd2  27528  noextend  27628  nodenselem5  27650  nosupbnd2lem1  27677  addsproplem1  27919  addsprop  27926  negsproplem1  27977  negsprop  27984  mulsproplemcbv  28058  mulsproplem1  28059  mulsprop  28073  precsexlemcbv  28147  precsexlem3  28150  sltonold  28200  pthdlem1  29694  wwlksnext  29821  clwwlknonex2lem1  30034  iunxunsn  32493  iunxunpr  32494  difres  32527  ofpreima2  32590  fzspl  32712  tocyc01  33075  ordtprsuni  33896  ordtcnvNEW  33897  carsgsigalem  34293  ballotlemfp1  34470  fsum2dsub  34585  reprsuc  34593  bnj941  34749  bnj944  34915  fineqvac  35074  subfacp1lem1  35147  cvmscld  35241  satf  35321  satfv1  35331  fmlasuc  35354  mrsubvrs  35490  mclsval  35531  rankaltopb  35943  rankung  36130  lindsadd  37583  lindsenlbs  37585  poimirlem1  37591  poimirlem2  37592  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem13  37603  poimirlem14  37604  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem26  37616  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  lshpnel2N  38949  paddfval  39762  hdmapval  41793  fzsplitnd  41941  lcmfunnnd  41971  metakunt24  42187  fsuppssind  42563  diophren  42783  omabs2  43303  tfsconcatrn  43313  tfsconcatrev  43319  iunrelexp0  43673  trclfvdecoml  43700  isotone1  44019  iunp1  45038  snunioo1  45489  dvmptfprodlem  45921  stoweidlem11  45988  stoweidlem26  46003  fourierdlem33  46117  fzopredsuc  47300  iccpartltu  47387  iccpartgt  47389  dfclnbgr2  47785  dfclnbgr4  47786  dfclnbgr3  47788  clnbupgr  47795  clnbgr0edg  47798  dfclnbgr5  47811  dfclnbgr6  47817  dfsclnbgr6  47819  cycl3grtri  47907  stgrclnbgr0  47925  lmod1zr  48417  tposres2  48803