Theorem uneq1d 4177

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968

This theorem is referenced by:  ifeq1  4535  preq1  4738  tpeq1  4747  tpeq2  4748  tpprceq3  4809  iunxdif3  5100  iununi  5104  resasplit  6779  fresaunres2  6781  fmptpr  7192  funresdfunsn  7209  ressuppssdif  8209  on2recsov  8705  sbthlem5  9126  fodomr  9167  domunfican  9359  fodomfir  9366  brwdom2  9611  ackbij1lem2  10258  ttukeylem3  10549  snunioo  13515  snunioc  13517  prunioo  13518  fzpred  13609  fseq1p1m1  13635  nn0split  13680  fz0sn0fz1  13682  fzo0sn0fzo1  13791  fzosplitpr  13812  s2prop  14943  s4prop  14946  fsum1p  15786  fprod1p  16001  setsval  17201  setsabs  17213  setscom  17214  prdsval  17502  prdsdsval  17525  prdsdsval2  17531  prdsdsval3  17532  mreexexlem3d  17691  mreexexlem4d  17692  estrres  18195  symg2bas  19425  symgvalstruct  19429  symgvalstructOLD  19430  evlseu  22125  ordtuni  23214  lfinun  23549  alexsubALTlem3  24073  ustssco  24239  trust  24254  ressprdsds  24397  xpsdsval  24407  nulmbl2  25585  uniioombllem3  25634  uniioombllem4  25635  plyeq0  26265  plyaddlem1  26267  plymullem1  26268  fta1lem  26364  vieta1lem2  26368  birthdaylem2  27010  noetasuplem2  27794  noxpordpred  28001  addsproplem1  28017  addsprop  28024  negsproplem1  28075  negsprop  28082  mulsproplemcbv  28156  mulsproplem1  28157  mulsprop  28171  precsexlemcbv  28245  precsexlem3  28248  edglnl  29175  iuninc  32581  pmtrcnel2  33093  tocycval  33111  cycpmco2rn  33128  difelcarsg  34292  actfunsnf1o  34598  reprsuc  34609  breprexplema  34624  bnj1416  35032  mclsval  35548  mclsax  35554  rankung  36148  topjoin  36348  bj-tageq  36959  finixpnum  37592  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem9  37616  poimirlem16  37623  poimirlem17  37624  poimirlem28  37635  mblfinlem2  37645  islshpsm  38962  lshpnel2N  38967  lkrlsp3  39086  pclfinclN  39933  dochsatshp  41434  metakunt24  42210  mapfzcons1  42705  iunrelexp0  43692  isotone1  44038  fiiuncl  45005  nnsplit  45308  fourierdlem32  46095  fzopred  47272  fzopredsuc  47273  dfsclnbgr6  47782  aacllem  49032