Theorem uneq1d 4114

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  ifeq1  4486  preq1  4694  tpeq1  4703  tpeq2  4704  tpprceq3  4767  iunxdif3  5055  iununi  5059  resasplit  6750  fresaunres2  6752  fmptpr  7175  funresdfunsn  7192  ressuppssdif  8195  on2recsov  8670  sbthlem5  9103  fodomr  9140  domunfican  9306  fodomfir  9312  brwdom2  9560  rankung  9866  ackbij1lem2  10291  ttukeylem3  10582  snunioo  13602  snunioc  13604  prunioo  13605  fzpred  13699  fseq1p1m1  13725  nn0split  13770  fz0sn0fz1  13772  fzo0sn0fzo1  13883  fzosplitpr  13905  s2prop  15051  s4prop  15054  fsum1p  15912  fprod1p  16128  setsval  17338  setsabs  17350  setscom  17351  prdsval  17619  prdsdsval  17642  prdsdsval2  17648  prdsdsval3  17649  mreexexlem3d  17813  mreexexlem4d  17814  estrres  18306  symg2bas  19600  symgvalstruct  19604  evlseu  22385  ordtuni  23501  lfinun  23837  alexsubALTlem3  24361  ustssco  24527  trust  24541  ressprdsds  24683  xpsdsval  24693  nulmbl2  25850  uniioombllem3  25899  uniioombllem4  25900  plyeq0  26523  plyaddlem1  26525  plymullem1  26526  fta1lem  26621  vieta1lem2  26627  birthdaylem2  27273  noetasuplem2  28084  noxpordpred  28332  addsproplem1  28348  addsprop  28355  negsproplem1  28407  negsprop  28414  mulsproplemcbv  28494  mulsproplem1  28495  mulsprop  28509  precsexlemcbv  28585  precsexlem3  28588  edglnl  29714  iuninc  33148  nn0diffz0  33379  pmtrcnel2  33644  tocycval  33662  cycpmco2rn  33679  dflringlem3  34021  dflring4  34023  evlextv  34167  difelcarsg  34935  actfunsnf1o  35226  reprsuc  35237  breprexplema  35252  bnj1416  35662  mclsval  36307  mclsax  36313  topjoin  37133  ttcsng  37287  ttcsntrsucg  37290  bj-tageq  37869  finixpnum  38508  poimirlem3  38521  poimirlem4  38522  poimirlem6  38524  poimirlem7  38525  poimirlem9  38527  poimirlem16  38534  poimirlem17  38535  poimirlem28  38546  mblfinlem2  38556  islshpsm  40017  lshpnel2N  40022  lkrlsp3  40141  pclfinclN  40987  dochsatshp  42488  mapfzcons1  43707  iunrelexp0  44687  isotone1  45033  fiiuncl  46051  nnsplit  46339  fourierdlem32  47118  fzopred  48362  fzopredsuc  48363  dfsclnbgr6  48925  aacllem  50908