Theorem uneq1d 4166

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  ifeq1  4485  preq1  4693  tpeq1  4702  tpeq2  4703  tpprceq3  4766  iunxdif3  5054  iununi  5058  resasplit  6752  fresaunres2  6754  fmptpr  7177  funresdfunsn  7194  ressuppssdif  8203  on2recsov  8678  sbthlem5  9111  fodomr  9148  domunfican  9314  fodomfir  9320  brwdom2  9568  rankung  9874  ackbij1lem2  10299  ttukeylem3  10590  snunioo  13610  snunioc  13612  prunioo  13613  fzpred  13707  fseq1p1m1  13733  nn0split  13778  fz0sn0fz1  13780  fzo0sn0fzo1  13891  fzosplitpr  13913  s2prop  15059  s4prop  15062  fsum1p  15920  fprod1p  16136  setsval  17346  setsabs  17358  setscom  17359  prdsval  17627  prdsdsval  17650  prdsdsval2  17656  prdsdsval3  17657  mreexexlem3d  17821  mreexexlem4d  17822  estrres  18314  symg2bas  19608  symgvalstruct  19612  evlseu  22393  ordtuni  23509  lfinun  23845  alexsubALTlem3  24369  ustssco  24535  trust  24549  ressprdsds  24691  xpsdsval  24701  nulmbl2  25858  uniioombllem3  25907  uniioombllem4  25908  plyeq0  26531  plyaddlem1  26533  plymullem1  26534  fta1lem  26629  vieta1lem2  26635  birthdaylem2  27281  noetasuplem2  28092  noxpordpred  28340  addsproplem1  28356  addsprop  28363  negsproplem1  28415  negsprop  28422  mulsproplemcbv  28502  mulsproplem1  28503  mulsprop  28517  precsexlemcbv  28593  precsexlem3  28596  edglnl  29722  iuninc  33198  nn0diffz0  33429  pmtrcnel2  33694  tocycval  33712  cycpmco2rn  33729  dflringlem3  34071  dflring4  34073  evlextv  34217  difelcarsg  34985  actfunsnf1o  35276  reprsuc  35287  breprexplema  35302  bnj1416  35712  mclsval  36371  mclsax  36377  topjoin  37196  ttcsng  37350  ttcsntrsucg  37353  bj-tageq  37932  finixpnum  38572  poimirlem3  38585  poimirlem4  38586  poimirlem6  38588  poimirlem7  38589  poimirlem9  38591  poimirlem16  38598  poimirlem17  38599  poimirlem28  38610  mblfinlem2  38620  islshpsm  40081  lshpnel2N  40086  lkrlsp3  40205  pclfinclN  41051  dochsatshp  42552  mapfzcons1  43772  iunrelexp0  44746  isotone1  45092  fiiuncl  46126  nnsplit  46414  fourierdlem32  47193  fzopred  48437  fzopredsuc  48438  dfsclnbgr6  49000  aacllem  50983