Theorem uneq1d 4130

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  ifeq1  4492  preq1  4697  tpeq1  4706  tpeq2  4707  tpprceq3  4768  iunxdif3  5059  iununi  5063  resasplit  6730  fresaunres2  6732  fmptpr  7146  funresdfunsn  7163  ressuppssdif  8164  on2recsov  8632  sbthlem5  9055  fodomr  9092  domunfican  9272  fodomfir  9279  brwdom2  9526  ackbij1lem2  10173  ttukeylem3  10464  snunioo  13439  snunioc  13441  prunioo  13442  fzpred  13533  fseq1p1m1  13559  nn0split  13604  fz0sn0fz1  13606  fzo0sn0fzo1  13716  fzosplitpr  13737  s2prop  14873  s4prop  14876  fsum1p  15719  fprod1p  15934  setsval  17137  setsabs  17149  setscom  17150  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  mreexexlem3d  17607  mreexexlem4d  17608  estrres  18100  symg2bas  19323  symgvalstruct  19327  evlseu  21990  ordtuni  23077  lfinun  23412  alexsubALTlem3  23936  ustssco  24102  trust  24117  ressprdsds  24259  xpsdsval  24269  nulmbl2  25437  uniioombllem3  25486  uniioombllem4  25487  plyeq0  26116  plyaddlem1  26118  plymullem1  26119  fta1lem  26215  vieta1lem2  26219  birthdaylem2  26862  noetasuplem2  27646  noxpordpred  27860  addsproplem1  27876  addsprop  27883  negsproplem1  27934  negsprop  27941  mulsproplemcbv  28018  mulsproplem1  28019  mulsprop  28033  precsexlemcbv  28108  precsexlem3  28111  edglnl  29070  iuninc  32489  pmtrcnel2  33047  tocycval  33065  cycpmco2rn  33082  difelcarsg  34301  actfunsnf1o  34595  reprsuc  34606  breprexplema  34621  bnj1416  35029  mclsval  35550  mclsax  35556  rankung  36154  topjoin  36353  bj-tageq  36964  finixpnum  37599  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem16  37630  poimirlem17  37631  poimirlem28  37642  mblfinlem2  37652  islshpsm  38973  lshpnel2N  38978  lkrlsp3  39097  pclfinclN  39944  dochsatshp  41445  mapfzcons1  42705  iunrelexp0  43691  isotone1  44037  fiiuncl  45059  nnsplit  45354  fourierdlem32  46137  fzopred  47320  fzopredsuc  47321  dfsclnbgr6  47855  aacllem  49787