Theorem uneq1d 4169

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  ifeq1  4489  preq1  4696  tpeq1  4705  tpeq2  4706  tpprceq3  4769  iunxdif3  5060  iununi  5064  resasplit  6782  fresaunres2  6784  fmptpr  7208  funresdfunsn  7225  ressuppssdif  8240  on2recsov  8715  sbthlem5  9148  fodomr  9185  domunfican  9351  fodomfir  9357  brwdom2  9604  rankung  9910  ackbij1lem2  10337  ttukeylem3  10628  snunioo  13649  snunioc  13651  prunioo  13652  fzpred  13746  fseq1p1m1  13772  nn0split  13817  fz0sn0fz1  13819  fzo0sn0fzo1  13930  fzosplitpr  13952  s2prop  15101  s4prop  15104  fsum1p  15963  fprod1p  16179  setsval  17389  setsabs  17401  setscom  17402  prdsval  17676  prdsdsval  17699  prdsdsval2  17705  prdsdsval3  17706  mreexexlem3d  17870  mreexexlem4d  17871  estrres  18363  symg2bas  19658  symgvalstruct  19662  evlseu  22447  ordtuni  23563  lfinun  23899  alexsubALTlem3  24423  ustssco  24589  trust  24603  ressprdsds  24745  xpsdsval  24755  nulmbl2  25912  uniioombllem3  25961  uniioombllem4  25962  plyeq0  26585  plyaddlem1  26587  plymullem1  26588  fta1lem  26683  vieta1lem2  26689  birthdaylem2  27337  noetasuplem2  28148  noxpordpred  28396  addsproplem1  28412  addsprop  28419  negsproplem1  28471  negsprop  28478  mulsproplemcbv  28558  mulsproplem1  28559  mulsprop  28573  precsexlemcbv  28649  precsexlem3  28652  edglnl  29778  iuninc  33253  nn0diffz0  33482  pmtrcnel2  33750  tocycval  33768  cycpmco2rn  33785  dflringlem3  34132  dflring4  34134  evlextv  34285  difelcarsg  35053  actfunsnf1o  35344  reprsuc  35355  breprexplema  35370  bnj1416  35780  mclsval  36536  mclsax  36542  topjoin  37368  ttcsng  37522  ttcsntrsucg  37525  bj-tageq  38104  finixpnum  38796  poimirlem3  38809  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem9  38815  poimirlem16  38822  poimirlem17  38823  poimirlem28  38834  mblfinlem2  38844  islshpsm  40303  lshpnel2N  40308  lkrlsp3  40427  pclfinclN  41273  dochsatshp  42774  mapfzcons1  43994  iunrelexp0  44963  isotone1  45309  fiiuncl  46356  nnsplit  46643  fourierdlem32  47422  fzopred  48666  fzopredsuc  48667  dfsclnbgr6  49229  aacllem  51367