Theorem uneq1d 4107

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  ifeq1  4470  preq1  4677  tpeq1  4686  tpeq2  4687  tpprceq3  4749  iunxdif3  5037  iununi  5041  resasplit  6710  fresaunres2  6712  fmptpr  7127  funresdfunsn  7144  ressuppssdif  8135  on2recsov  8604  sbthlem5  9029  fodomr  9066  domunfican  9232  fodomfir  9238  brwdom2  9488  ackbij1lem2  10142  ttukeylem3  10433  snunioo  13431  snunioc  13433  prunioo  13434  fzpred  13526  fseq1p1m1  13552  nn0split  13597  fz0sn0fz1  13599  fzo0sn0fzo1  13710  fzosplitpr  13732  s2prop  14869  s4prop  14872  fsum1p  15715  fprod1p  15933  setsval  17137  setsabs  17149  setscom  17150  prdsval  17418  prdsdsval  17441  prdsdsval2  17447  prdsdsval3  17448  mreexexlem3d  17612  mreexexlem4d  17613  estrres  18105  symg2bas  19368  symgvalstruct  19372  evlseu  22061  ordtuni  23155  lfinun  23490  alexsubALTlem3  24014  ustssco  24180  trust  24194  ressprdsds  24336  xpsdsval  24346  nulmbl2  25503  uniioombllem3  25552  uniioombllem4  25553  plyeq0  26176  plyaddlem1  26178  plymullem1  26179  fta1lem  26273  vieta1lem2  26277  birthdaylem2  26916  noetasuplem2  27698  noxpordpred  27945  addsproplem1  27961  addsprop  27968  negsproplem1  28020  negsprop  28027  mulsproplemcbv  28107  mulsproplem1  28108  mulsprop  28122  precsexlemcbv  28198  precsexlem3  28201  edglnl  29212  iuninc  32630  nn0diffz0  32867  pmtrcnel2  33151  tocycval  33169  cycpmco2rn  33186  evlextv  33686  difelcarsg  34454  actfunsnf1o  34748  reprsuc  34759  breprexplema  34774  bnj1416  35181  mclsval  35745  mclsax  35751  rankung  36348  topjoin  36547  ttcsng  36701  ttcsntrsucg  36704  bj-tageq  37283  finixpnum  37926  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem16  37957  poimirlem17  37958  poimirlem28  37969  mblfinlem2  37979  islshpsm  39426  lshpnel2N  39431  lkrlsp3  39550  pclfinclN  40396  dochsatshp  41897  mapfzcons1  43149  iunrelexp0  44129  isotone1  44475  fiiuncl  45496  nnsplit  45788  fourierdlem32  46567  fzopred  47771  fzopredsuc  47772  dfsclnbgr6  48334  aacllem  50276