Theorem uneq1d 4121

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  ifeq1  4493  preq1  4701  tpeq1  4710  tpeq2  4711  tpprceq3  4774  iunxdif3  5063  iununi  5067  resasplit  6752  fresaunres2  6754  fmptpr  7174  funresdfunsn  7191  ressuppssdif  8183  on2recsov  8656  sbthlem5  9082  fodomr  9119  domunfican  9284  fodomfir  9290  brwdom2  9538  ackbij1lem2  10215  ttukeylem3  10506  snunioo  13517  snunioc  13519  prunioo  13520  fzpred  13613  fseq1p1m1  13639  nn0split  13684  fz0sn0fz1  13686  fzo0sn0fzo1  13797  fzosplitpr  13819  s2prop  14964  s4prop  14967  fsum1p  15823  fprod1p  16041  setsval  17245  setsabs  17257  setscom  17258  prdsval  17526  prdsdsval  17549  prdsdsval2  17555  prdsdsval3  17556  mreexexlem3d  17720  mreexexlem4d  17721  estrres  18213  symg2bas  19487  symgvalstruct  19491  evlseu  22264  ordtuni  23377  lfinun  23713  alexsubALTlem3  24237  ustssco  24403  trust  24417  ressprdsds  24559  xpsdsval  24569  nulmbl2  25726  uniioombllem3  25775  uniioombllem4  25776  plyeq0  26399  plyaddlem1  26401  plymullem1  26402  fta1lem  26499  vieta1lem2  26503  birthdaylem2  27148  noetasuplem2  27929  noxpordpred  28177  addsproplem1  28193  addsprop  28200  negsproplem1  28252  negsprop  28259  mulsproplemcbv  28339  mulsproplem1  28340  mulsprop  28354  precsexlemcbv  28430  precsexlem3  28433  edglnl  29524  iuninc  32952  nn0diffz0  33185  pmtrcnel2  33450  tocycval  33468  cycpmco2rn  33485  dflringlem3  33826  dflring4  33828  evlextv  33972  difelcarsg  34741  actfunsnf1o  35032  reprsuc  35043  breprexplema  35058  bnj1416  35468  mclsval  36068  mclsax  36074  rankung  36671  topjoin  36909  ttcsng  37063  ttcsntrsucg  37066  bj-tageq  37645  finixpnum  38289  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem16  38320  poimirlem17  38321  poimirlem28  38332  mblfinlem2  38342  islshpsm  39787  lshpnel2N  39792  lkrlsp3  39911  pclfinclN  40757  dochsatshp  42258  mapfzcons1  43481  iunrelexp0  44461  isotone1  44807  fiiuncl  45818  nnsplit  46107  fourierdlem32  46886  fzopred  48093  fzopredsuc  48094  dfsclnbgr6  48656  aacllem  50654