Theorem uneq2d 4164

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954

This theorem is referenced by:  ifeq2  4534  tpeq3  4749  iununi  5103  sucprc  6441  unisucs  6442  resasplit  6762  fvun1  6983  fmptapd  7172  fndifnfp  7177  fvunsn  7180  fnsnsplit  7185  f1ofvswap  7308  oev2  8527  oarec  8566  ralxpmap  8894  sbthlem5  9091  sbthlem6  9092  domss2  9140  dif1en  9164  dif1enOLD  9166  unfi  9176  domunfican  9324  fiint  9328  fodomfi  9329  pm54.43  10000  kmlem2  10150  kmlem11  10159  ackbij1lem1  10219  fin23lem26  10324  axdc3lem4  10452  fpwwe2lem12  10641  wunex2  10737  wuncval2  10746  ioounsn  13460  snunico  13462  ioojoin  13466  fzsuc  13554  fseq1p1m1  13581  fseq1m1p1  13582  fzosplitsnm1  13713  fzosplitsn  13746  fzosplitpr  13747  fzosplitprm1  13748  hashfun  14403  resunimafz0  14410  s4prop  14867  fsumm1  15703  climcndslem1  15801  fprodm1  15917  ruclem4  16183  lcmfunsnlem1  16580  lcmfunsnlem2lem1  16581  lcmfunsnlem2lem2  16582  lcmfunsnlem2  16583  lcmfunsn  16587  vdwap1  16916  setscom  17119  setsidvald  17138  setsidvaldOLD  17139  mreexmrid  17593  mreexexlemd  17594  mreexexlem2d  17595  cnvtsr  18547  dprd2da  19955  dmdprdsplit2lem  19958  lspun0  20768  lbsextlem4  20921  cmpcld  23128  comppfsc  23258  trfil2  23613  cldsubg  23837  tsmsres  23870  icccmplem2  24561  uniioombllem4  25337  ppiprm  26889  chtprm  26891  pntrsumbnd2  27304  noextend  27403  nodenselem5  27425  nosupbnd2lem1  27452  addsproplem1  27689  addsprop  27696  negsproplem1  27739  negsprop  27746  mulsproplemcbv  27808  mulsproplem1  27809  mulsprop  27823  precsexlemcbv  27889  precsexlem3  27892  sltonold  27924  pthdlem1  29288  wwlksnext  29412  clwwlknonex2lem1  29625  iunxunsn  32063  iunxunpr  32064  difres  32096  ofpreima2  32156  fzspl  32266  tocyc01  32545  ordtprsuni  33195  ordtcnvNEW  33196  carsgsigalem  33610  ballotlemfp1  33786  fsum2dsub  33915  reprsuc  33923  bnj941  34079  bnj944  34245  fineqvac  34393  subfacp1lem1  34466  cvmscld  34560  satf  34640  satfv1  34650  fmlasuc  34673  mrsubvrs  34809  mclsval  34850  rankaltopb  35253  rankung  35440  lindsadd  36786  lindsenlbs  36788  poimirlem1  36794  poimirlem2  36795  poimirlem4  36797  poimirlem6  36799  poimirlem7  36800  poimirlem8  36801  poimirlem13  36806  poimirlem14  36807  poimirlem16  36809  poimirlem17  36810  poimirlem18  36811  poimirlem19  36812  poimirlem20  36813  poimirlem21  36814  poimirlem22  36815  poimirlem26  36819  poimirlem28  36821  poimirlem31  36824  poimirlem32  36825  lshpnel2N  38160  paddfval  38973  hdmapval  41004  fzsplitnd  41156  lcmfunnnd  41185  metakunt24  41316  fsuppssind  41469  diophren  41855  omabs2  42386  tfsconcatrn  42396  tfsconcatrev  42402  iunrelexp0  42757  trclfvdecoml  42784  isotone1  43103  iunp1  44056  snunioo1  44525  dvmptfprodlem  44960  stoweidlem11  45027  stoweidlem26  45042  fourierdlem33  45156  fzopredsuc  46331  iccpartltu  46393  iccpartgt  46395  lmod1zr  47263