Theorem uneq1d 4120

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

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

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 3440  df-un 3910

This theorem is referenced by:  ifeq1  4482  preq1  4687  tpeq1  4696  tpeq2  4697  tpprceq3  4758  iunxdif3  5047  iununi  5051  resasplit  6698  fresaunres2  6700  fmptpr  7112  funresdfunsn  7129  ressuppssdif  8125  on2recsov  8593  sbthlem5  9015  fodomr  9052  domunfican  9230  fodomfir  9237  brwdom2  9484  ackbij1lem2  10133  ttukeylem3  10424  snunioo  13399  snunioc  13401  prunioo  13402  fzpred  13493  fseq1p1m1  13519  nn0split  13564  fz0sn0fz1  13566  fzo0sn0fzo1  13676  fzosplitpr  13697  s2prop  14832  s4prop  14835  fsum1p  15678  fprod1p  15893  setsval  17096  setsabs  17108  setscom  17109  prdsval  17377  prdsdsval  17400  prdsdsval2  17406  prdsdsval3  17407  mreexexlem3d  17570  mreexexlem4d  17571  estrres  18063  symg2bas  19290  symgvalstruct  19294  evlseu  22006  ordtuni  23093  lfinun  23428  alexsubALTlem3  23952  ustssco  24118  trust  24133  ressprdsds  24275  xpsdsval  24285  nulmbl2  25453  uniioombllem3  25502  uniioombllem4  25503  plyeq0  26132  plyaddlem1  26134  plymullem1  26135  fta1lem  26231  vieta1lem2  26235  birthdaylem2  26878  noetasuplem2  27662  noxpordpred  27883  addsproplem1  27899  addsprop  27906  negsproplem1  27957  negsprop  27964  mulsproplemcbv  28041  mulsproplem1  28042  mulsprop  28056  precsexlemcbv  28131  precsexlem3  28134  edglnl  29106  iuninc  32522  pmtrcnel2  33045  tocycval  33063  cycpmco2rn  33080  difelcarsg  34280  actfunsnf1o  34574  reprsuc  34585  breprexplema  34600  bnj1416  35008  mclsval  35538  mclsax  35544  rankung  36142  topjoin  36341  bj-tageq  36952  finixpnum  37587  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem9  37611  poimirlem16  37618  poimirlem17  37619  poimirlem28  37630  mblfinlem2  37640  islshpsm  38961  lshpnel2N  38966  lkrlsp3  39085  pclfinclN  39932  dochsatshp  41433  mapfzcons1  42693  iunrelexp0  43678  isotone1  44024  fiiuncl  45046  nnsplit  45341  fourierdlem32  46124  fzopred  47310  fzopredsuc  47311  dfsclnbgr6  47846  aacllem  49790