Theorem uneq1d 4116

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  ifeq1  4480  preq1  4687  tpeq1  4696  tpeq2  4697  tpprceq3  4757  iunxdif3  5047  iununi  5051  resasplit  6701  fresaunres2  6703  fmptpr  7115  funresdfunsn  7132  ressuppssdif  8124  on2recsov  8592  sbthlem5  9015  fodomr  9052  domunfican  9217  fodomfir  9223  brwdom2  9470  ackbij1lem2  10122  ttukeylem3  10413  snunioo  13385  snunioc  13387  prunioo  13388  fzpred  13479  fseq1p1m1  13505  nn0split  13550  fz0sn0fz1  13552  fzo0sn0fzo1  13662  fzosplitpr  13684  s2prop  14821  s4prop  14824  fsum1p  15667  fprod1p  15882  setsval  17085  setsabs  17097  setscom  17098  prdsval  17366  prdsdsval  17389  prdsdsval2  17395  prdsdsval3  17396  mreexexlem3d  17560  mreexexlem4d  17561  estrres  18053  symg2bas  19313  symgvalstruct  19317  evlseu  22029  ordtuni  23125  lfinun  23460  alexsubALTlem3  23984  ustssco  24150  trust  24164  ressprdsds  24306  xpsdsval  24316  nulmbl2  25484  uniioombllem3  25533  uniioombllem4  25534  plyeq0  26163  plyaddlem1  26165  plymullem1  26166  fta1lem  26262  vieta1lem2  26266  birthdaylem2  26909  noetasuplem2  27693  noxpordpred  27916  addsproplem1  27932  addsprop  27939  negsproplem1  27990  negsprop  27997  mulsproplemcbv  28074  mulsproplem1  28075  mulsprop  28089  precsexlemcbv  28164  precsexlem3  28167  edglnl  29142  iuninc  32561  nn0diffz0  32802  pmtrcnel2  33100  tocycval  33118  cycpmco2rn  33135  evlextv  33635  difelcarsg  34395  actfunsnf1o  34689  reprsuc  34700  breprexplema  34715  bnj1416  35123  mclsval  35679  mclsax  35685  rankung  36282  topjoin  36481  bj-tageq  37093  finixpnum  37718  poimirlem3  37736  poimirlem4  37737  poimirlem6  37739  poimirlem7  37740  poimirlem9  37742  poimirlem16  37749  poimirlem17  37750  poimirlem28  37761  mblfinlem2  37771  islshpsm  39152  lshpnel2N  39157  lkrlsp3  39276  pclfinclN  40122  dochsatshp  41623  mapfzcons1  42874  iunrelexp0  43859  isotone1  44205  fiiuncl  45226  nnsplit  45519  fourierdlem32  46299  fzopred  47484  fzopredsuc  47485  dfsclnbgr6  48020  aacllem  49962