Theorem uneq1d 4108

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  ifeq1  4471  preq1  4678  tpeq1  4687  tpeq2  4688  tpprceq3  4748  iunxdif3  5038  iununi  5042  resasplit  6704  fresaunres2  6706  fmptpr  7120  funresdfunsn  7137  ressuppssdif  8128  on2recsov  8597  sbthlem5  9022  fodomr  9059  domunfican  9225  fodomfir  9231  brwdom2  9481  ackbij1lem2  10133  ttukeylem3  10424  snunioo  13422  snunioc  13424  prunioo  13425  fzpred  13517  fseq1p1m1  13543  nn0split  13588  fz0sn0fz1  13590  fzo0sn0fzo1  13701  fzosplitpr  13723  s2prop  14860  s4prop  14863  fsum1p  15706  fprod1p  15924  setsval  17128  setsabs  17140  setscom  17141  prdsval  17409  prdsdsval  17432  prdsdsval2  17438  prdsdsval3  17439  mreexexlem3d  17603  mreexexlem4d  17604  estrres  18096  symg2bas  19359  symgvalstruct  19363  evlseu  22071  ordtuni  23165  lfinun  23500  alexsubALTlem3  24024  ustssco  24190  trust  24204  ressprdsds  24346  xpsdsval  24356  nulmbl2  25513  uniioombllem3  25562  uniioombllem4  25563  plyeq0  26186  plyaddlem1  26188  plymullem1  26189  fta1lem  26284  vieta1lem2  26288  birthdaylem2  26929  noetasuplem2  27712  noxpordpred  27959  addsproplem1  27975  addsprop  27982  negsproplem1  28034  negsprop  28041  mulsproplemcbv  28121  mulsproplem1  28122  mulsprop  28136  precsexlemcbv  28212  precsexlem3  28215  edglnl  29226  iuninc  32645  nn0diffz0  32882  pmtrcnel2  33166  tocycval  33184  cycpmco2rn  33201  evlextv  33701  difelcarsg  34470  actfunsnf1o  34764  reprsuc  34775  breprexplema  34790  bnj1416  35197  mclsval  35761  mclsax  35767  rankung  36364  topjoin  36563  ttcsng  36717  ttcsntrsucg  36720  bj-tageq  37299  finixpnum  37940  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem16  37971  poimirlem17  37972  poimirlem28  37983  mblfinlem2  37993  islshpsm  39440  lshpnel2N  39445  lkrlsp3  39564  pclfinclN  40410  dochsatshp  41911  mapfzcons1  43163  iunrelexp0  44147  isotone1  44493  fiiuncl  45514  nnsplit  45806  fourierdlem32  46585  fzopred  47783  fzopredsuc  47784  dfsclnbgr6  48346  aacllem  50288