Theorem uneq1d 4118

Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq1d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq1 4112	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   = wceq 1559   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907

This theorem is referenced by:  ifeq1  4481  preq1  4689  tpeq1  4698  tpeq2  4699  tpprceq3  4761  iunxdif3  5049  iununi  5053  resasplit  6729  fresaunres2  6731  fmptpr  7151  funresdfunsn  7168  ressuppssdif  8159  on2recsov  8632  sbthlem5  9057  fodomr  9094  domunfican  9260  fodomfir  9266  brwdom2  9515  ackbij1lem2  10170  ttukeylem3  10462  snunioo  13476  snunioc  13478  prunioo  13479  fzpred  13571  fseq1p1m1  13597  nn0split  13642  fz0sn0fz1  13644  fzo0sn0fzo1  13755  fzosplitpr  13777  s2prop  14914  s4prop  14917  fsum1p  15771  fprod1p  15989  setsval  17194  setsabs  17206  setscom  17207  prdsval  17475  prdsdsval  17498  prdsdsval2  17504  prdsdsval3  17505  mreexexlem3d  17669  mreexexlem4d  17670  estrres  18162  symg2bas  19424  symgvalstruct  19428  evlseu  22124  ordtuni  23238  lfinun  23573  alexsubALTlem3  24097  ustssco  24263  trust  24277  ressprdsds  24419  xpsdsval  24429  nulmbl2  25586  uniioombllem3  25635  uniioombllem4  25636  plyeq0  26259  plyaddlem1  26261  plymullem1  26262  fta1lem  26359  vieta1lem2  26363  birthdaylem2  27005  noetasuplem2  27786  noxpordpred  28034  addsproplem1  28050  addsprop  28057  negsproplem1  28109  negsprop  28116  mulsproplemcbv  28196  mulsproplem1  28197  mulsprop  28211  precsexlemcbv  28287  precsexlem3  28290  edglnl  29301  iuninc  32720  nn0diffz0  32957  pmtrcnel2  33231  tocycval  33249  cycpmco2rn  33266  dflringlem3  33653  dflring4  33655  evlextv  33800  difelcarsg  34568  actfunsnf1o  34859  reprsuc  34870  breprexplema  34885  bnj1416  35295  mclsval  35874  mclsax  35880  rankung  36477  topjoin  36686  ttcsng  36840  ttcsntrsucg  36843  bj-tageq  37422  finixpnum  38065  poimirlem3  38083  poimirlem4  38084  poimirlem6  38086  poimirlem7  38087  poimirlem9  38089  poimirlem16  38096  poimirlem17  38097  poimirlem28  38108  mblfinlem2  38118  islshpsm  39565  lshpnel2N  39570  lkrlsp3  39689  pclfinclN  40535  dochsatshp  42036  mapfzcons1  43259  iunrelexp0  44239  isotone1  44585  fiiuncl  45606  nnsplit  45895  fourierdlem32  46674  fzopred  47878  fzopredsuc  47879  dfsclnbgr6  48441  aacllem  50383