Theorem uneq1d 4089

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

Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3879

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  ifeq1  4429  preq1  4629  tpeq1  4638  tpeq2  4639  tpprceq3  4697  iunxdif3  4980  iununi  4984  resasplit  6522  fresaunres2  6524  fmptpr  6911  funresdfunsn  6928  ressuppssdif  7834  sbthlem5  8615  fodomr  8652  domunfican  8775  brwdom2  9021  ackbij1lem2  9632  ttukeylem3  9922  snunioo  12856  snunioc  12858  prunioo  12859  fzpred  12950  fseq1p1m1  12976  nn0split  13017  fz0sn0fz1  13019  fzo0sn0fzo1  13121  fzosplitpr  13141  s2prop  14260  s4prop  14263  fsum1p  15100  fprod1p  15314  setsval  16505  setsabs  16518  setscom  16519  prdsval  16720  prdsdsval  16743  prdsdsval2  16749  prdsdsval3  16750  mreexexlem3d  16909  mreexexlem4d  16910  estrres  17381  symg2bas  18513  symgvalstruct  18517  evlseu  20755  ordtuni  21795  lfinun  22130  alexsubALTlem3  22654  ustssco  22820  trust  22835  ressprdsds  22978  xpsdsval  22988  nulmbl2  24140  uniioombllem3  24189  uniioombllem4  24190  plyeq0  24808  plyaddlem1  24810  plymullem1  24811  fta1lem  24903  vieta1lem2  24907  birthdaylem2  25538  edglnl  26936  iuninc  30324  pmtrcnel2  30784  tocycval  30800  cycpmco2rn  30817  difelcarsg  31678  actfunsnf1o  31985  reprsuc  31996  breprexplema  32011  bnj1416  32421  mclsval  32923  mclsax  32929  rankung  33740  topjoin  33826  bj-tageq  34412  finixpnum  35042  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem16  35073  poimirlem17  35074  poimirlem28  35085  mblfinlem2  35095  islshpsm  36276  lshpnel2N  36281  lkrlsp3  36400  pclfinclN  37246  dochsatshp  38747  metakunt24  39373  mapfzcons1  39658  iunrelexp0  40403  isotone1  40751  fiiuncl  41699  nnsplit  41990  fourierdlem32  42781  fzopred  43879  fzopredsuc  43880  aacllem  45329