Theorem uneq1d 3989

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

Syntax hints:   → wi 4   = wceq 1601   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797

This theorem is referenced by:  ifeq1  4311  preq1  4500  tpeq1  4509  tpeq2  4510  tpprceq3  4566  iunxdif3  4840  iununi  4844  resasplit  6324  fresaunres2  6326  fmptpr  6705  funresdfunsn  6726  ressuppssdif  7597  sbthlem5  8362  fodomr  8399  domunfican  8521  brwdom2  8767  cdaval  9327  ackbij1lem2  9378  ttukeylem3  9668  snunioo  12615  snunioc  12617  prunioo  12618  fzpred  12706  fseq1p1m1  12732  nn0split  12773  fz0sn0fz1  12775  fzo0sn0fzo1  12876  fzosplitpr  12896  s2prop  14058  s4prop  14061  fsum1p  14889  fprod1p  15101  setsval  16285  setsabs  16298  setscom  16299  prdsval  16501  prdsdsval  16524  prdsdsval2  16530  prdsdsval3  16531  mreexexlem3d  16692  mreexexlem4d  16693  estrresOLD  17164  estrres  17165  symg2bas  18201  evlseu  19912  ordtuni  21402  lfinun  21737  alexsubALTlem3  22261  ustssco  22426  trust  22441  ressprdsds  22584  xpsdsval  22594  nulmbl2  23740  uniioombllem3  23789  uniioombllem4  23790  plyeq0  24404  plyaddlem1  24406  plymullem1  24407  fta1lem  24499  vieta1lem2  24503  birthdaylem2  25131  edglnl  26492  iuninc  29941  difelcarsg  30970  actfunsnf1o  31284  reprsuc  31295  breprexplema  31310  bnj1416  31706  mclsval  32059  mclsax  32065  rankung  32862  topjoin  32948  bj-tageq  33536  finixpnum  34019  poimirlem3  34038  poimirlem4  34039  poimirlem6  34041  poimirlem7  34042  poimirlem9  34044  poimirlem16  34051  poimirlem17  34052  poimirlem28  34063  mblfinlem2  34073  islshpsm  35134  lshpnel2N  35139  lkrlsp3  35258  pclfinclN  36104  dochsatshp  37605  mapfzcons1  38240  iunrelexp0  38951  isotone1  39302  fiiuncl  40165  nnsplit  40482  fourierdlem32  41283  fzopred  42364  fzopredsuc  42365  aacllem  43653