Theorem uneq1d 4119

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  ifeq1  4483  preq1  4690  tpeq1  4699  tpeq2  4700  tpprceq3  4760  iunxdif3  5050  iununi  5054  resasplit  6704  fresaunres2  6706  fmptpr  7118  funresdfunsn  7135  ressuppssdif  8127  on2recsov  8596  sbthlem5  9019  fodomr  9056  domunfican  9222  fodomfir  9228  brwdom2  9478  ackbij1lem2  10130  ttukeylem3  10421  snunioo  13394  snunioc  13396  prunioo  13397  fzpred  13488  fseq1p1m1  13514  nn0split  13559  fz0sn0fz1  13561  fzo0sn0fzo1  13671  fzosplitpr  13693  s2prop  14830  s4prop  14833  fsum1p  15676  fprod1p  15891  setsval  17094  setsabs  17106  setscom  17107  prdsval  17375  prdsdsval  17398  prdsdsval2  17404  prdsdsval3  17405  mreexexlem3d  17569  mreexexlem4d  17570  estrres  18062  symg2bas  19322  symgvalstruct  19326  evlseu  22038  ordtuni  23134  lfinun  23469  alexsubALTlem3  23993  ustssco  24159  trust  24173  ressprdsds  24315  xpsdsval  24325  nulmbl2  25493  uniioombllem3  25542  uniioombllem4  25543  plyeq0  26172  plyaddlem1  26174  plymullem1  26175  fta1lem  26271  vieta1lem2  26275  birthdaylem2  26918  noetasuplem2  27702  noxpordpred  27949  addsproplem1  27965  addsprop  27972  negsproplem1  28024  negsprop  28031  mulsproplemcbv  28111  mulsproplem1  28112  mulsprop  28126  precsexlemcbv  28202  precsexlem3  28205  edglnl  29216  iuninc  32635  nn0diffz0  32874  pmtrcnel2  33172  tocycval  33190  cycpmco2rn  33207  evlextv  33707  difelcarsg  34467  actfunsnf1o  34761  reprsuc  34772  breprexplema  34787  bnj1416  35195  mclsval  35757  mclsax  35763  rankung  36360  topjoin  36559  bj-tageq  37177  finixpnum  37806  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem16  37837  poimirlem17  37838  poimirlem28  37849  mblfinlem2  37859  islshpsm  39240  lshpnel2N  39245  lkrlsp3  39364  pclfinclN  40210  dochsatshp  41711  mapfzcons1  42959  iunrelexp0  43943  isotone1  44289  fiiuncl  45310  nnsplit  45603  fourierdlem32  46383  fzopred  47568  fzopredsuc  47569  dfsclnbgr6  48104  aacllem  50046