Theorem uneq1d 4126

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

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

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 3446  df-un 3916

This theorem is referenced by:  ifeq1  4488  preq1  4693  tpeq1  4702  tpeq2  4703  tpprceq3  4764  iunxdif3  5054  iununi  5058  resasplit  6712  fresaunres2  6714  fmptpr  7128  funresdfunsn  7145  ressuppssdif  8141  on2recsov  8609  sbthlem5  9032  fodomr  9069  domunfican  9248  fodomfir  9255  brwdom2  9502  ackbij1lem2  10149  ttukeylem3  10440  snunioo  13415  snunioc  13417  prunioo  13418  fzpred  13509  fseq1p1m1  13535  nn0split  13580  fz0sn0fz1  13582  fzo0sn0fzo1  13692  fzosplitpr  13713  s2prop  14849  s4prop  14852  fsum1p  15695  fprod1p  15910  setsval  17113  setsabs  17125  setscom  17126  prdsval  17394  prdsdsval  17417  prdsdsval2  17423  prdsdsval3  17424  mreexexlem3d  17583  mreexexlem4d  17584  estrres  18076  symg2bas  19299  symgvalstruct  19303  evlseu  21966  ordtuni  23053  lfinun  23388  alexsubALTlem3  23912  ustssco  24078  trust  24093  ressprdsds  24235  xpsdsval  24245  nulmbl2  25413  uniioombllem3  25462  uniioombllem4  25463  plyeq0  26092  plyaddlem1  26094  plymullem1  26095  fta1lem  26191  vieta1lem2  26195  birthdaylem2  26838  noetasuplem2  27622  noxpordpred  27836  addsproplem1  27852  addsprop  27859  negsproplem1  27910  negsprop  27917  mulsproplemcbv  27994  mulsproplem1  27995  mulsprop  28009  precsexlemcbv  28084  precsexlem3  28087  edglnl  29046  iuninc  32462  pmtrcnel2  33020  tocycval  33038  cycpmco2rn  33055  difelcarsg  34274  actfunsnf1o  34568  reprsuc  34579  breprexplema  34594  bnj1416  35002  mclsval  35523  mclsax  35529  rankung  36127  topjoin  36326  bj-tageq  36937  finixpnum  37572  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem9  37596  poimirlem16  37603  poimirlem17  37604  poimirlem28  37615  mblfinlem2  37625  islshpsm  38946  lshpnel2N  38951  lkrlsp3  39070  pclfinclN  39917  dochsatshp  41418  mapfzcons1  42678  iunrelexp0  43664  isotone1  44010  fiiuncl  45032  nnsplit  45327  fourierdlem32  46110  fzopred  47296  fzopredsuc  47297  dfsclnbgr6  47831  aacllem  49763