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 1542   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954

This theorem is referenced by:  ifeq2  4534  tpeq3  4749  iununi  5103  sucprc  6441  unisucs  6442  resasplit  6762  fvun1  6983  fmptapd  7169  fndifnfp  7174  fvunsn  7177  fnsnsplit  7182  f1ofvswap  7304  oev2  8523  oarec  8562  ralxpmap  8890  sbthlem5  9087  sbthlem6  9088  domss2  9136  dif1en  9160  dif1enOLD  9162  unfi  9172  domunfican  9320  fiint  9324  fodomfi  9325  pm54.43  9996  kmlem2  10146  kmlem11  10155  ackbij1lem1  10215  fin23lem26  10320  axdc3lem4  10448  fpwwe2lem12  10637  wunex2  10733  wuncval2  10742  ioounsn  13454  snunico  13456  ioojoin  13460  fzsuc  13548  fseq1p1m1  13575  fseq1m1p1  13576  fzosplitsnm1  13707  fzosplitsn  13740  fzosplitpr  13741  fzosplitprm1  13742  hashfun  14397  resunimafz0  14404  s4prop  14861  fsumm1  15697  climcndslem1  15795  fprodm1  15911  ruclem4  16177  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfunsn  16581  vdwap1  16910  setscom  17113  setsidvald  17132  setsidvaldOLD  17133  mreexmrid  17587  mreexexlemd  17588  mreexexlem2d  17589  cnvtsr  18541  dprd2da  19912  dmdprdsplit2lem  19915  lspun0  20622  lbsextlem4  20774  cmpcld  22906  comppfsc  23036  trfil2  23391  cldsubg  23615  tsmsres  23648  icccmplem2  24339  uniioombllem4  25103  ppiprm  26655  chtprm  26657  pntrsumbnd2  27070  noextend  27169  nodenselem5  27191  nosupbnd2lem1  27218  addsproplem1  27453  addsprop  27460  negsproplem1  27502  negsprop  27509  mulsproplemcbv  27571  mulsproplem1  27572  mulsprop  27586  precsexlemcbv  27652  precsexlem3  27655  pthdlem1  29023  wwlksnext  29147  clwwlknonex2lem1  29360  iunxunsn  31798  iunxunpr  31799  difres  31831  ofpreima2  31891  fzspl  32001  tocyc01  32277  ordtprsuni  32899  ordtcnvNEW  32900  carsgsigalem  33314  ballotlemfp1  33490  fsum2dsub  33619  reprsuc  33627  bnj941  33783  bnj944  33949  fineqvac  34097  subfacp1lem1  34170  cvmscld  34264  satf  34344  satfv1  34354  fmlasuc  34377  mrsubvrs  34513  mclsval  34554  rankaltopb  34951  rankung  35138  lindsadd  36481  lindsenlbs  36483  poimirlem1  36489  poimirlem2  36490  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem13  36501  poimirlem14  36502  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem26  36514  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  lshpnel2N  37855  paddfval  38668  hdmapval  40699  fzsplitnd  40848  lcmfunnnd  40877  metakunt24  41008  fsuppssind  41165  diophren  41551  omabs2  42082  tfsconcatrn  42092  tfsconcatrev  42098  iunrelexp0  42453  trclfvdecoml  42480  isotone1  42799  iunp1  43753  snunioo1  44225  dvmptfprodlem  44660  stoweidlem11  44727  stoweidlem26  44742  fourierdlem33  44856  fzopredsuc  46031  iccpartltu  46093  iccpartgt  46095  lmod1zr  47174