Theorem uneq1d 4097

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

Syntax hints:   → wi 4   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  ifeq1  4458  preq1  4665  tpeq1  4674  tpeq2  4675  tpprceq3  4737  iunxdif3  5024  iununi  5028  resasplit  6697  fresaunres2  6699  fmptpr  7116  funresdfunsn  7133  ressuppssdif  8125  on2recsov  8594  sbthlem5  9019  fodomr  9056  domunfican  9222  fodomfir  9228  brwdom2  9478  ackbij1lem2  10133  ttukeylem3  10424  snunioo  13422  snunioc  13424  prunioo  13425  fzpred  13517  fseq1p1m1  13543  nn0split  13588  fz0sn0fz1  13590  fzo0sn0fzo1  13701  fzosplitpr  13723  s2prop  14860  s4prop  14863  fsum1p  15706  fprod1p  15924  setsval  17128  setsabs  17140  setscom  17141  prdsval  17409  prdsdsval  17432  prdsdsval2  17438  prdsdsval3  17439  mreexexlem3d  17603  mreexexlem4d  17604  estrres  18096  symg2bas  19359  symgvalstruct  19363  evlseu  22059  ordtuni  23173  lfinun  23508  alexsubALTlem3  24032  ustssco  24198  trust  24212  ressprdsds  24354  xpsdsval  24364  nulmbl2  25521  uniioombllem3  25570  uniioombllem4  25571  plyeq0  26194  plyaddlem1  26196  plymullem1  26197  fta1lem  26291  vieta1lem2  26295  birthdaylem2  26934  noetasuplem2  27716  noxpordpred  27963  addsproplem1  27979  addsprop  27986  negsproplem1  28038  negsprop  28045  mulsproplemcbv  28125  mulsproplem1  28126  mulsprop  28140  precsexlemcbv  28216  precsexlem3  28219  edglnl  29230  iuninc  32649  nn0diffz0  32886  pmtrcnel2  33171  tocycval  33189  cycpmco2rn  33206  evlextv  33726  difelcarsg  34494  actfunsnf1o  34788  reprsuc  34799  breprexplema  34814  bnj1416  35221  mclsval  35791  mclsax  35797  rankung  36394  topjoin  36593  ttcsng  36747  ttcsntrsucg  36750  bj-tageq  37329  finixpnum  37972  poimirlem3  37990  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem16  38003  poimirlem17  38004  poimirlem28  38015  mblfinlem2  38025  islshpsm  39472  lshpnel2N  39477  lkrlsp3  39596  pclfinclN  40442  dochsatshp  41943  mapfzcons1  43166  iunrelexp0  44146  isotone1  44492  fiiuncl  45513  nnsplit  45803  fourierdlem32  46582  fzopred  47786  fzopredsuc  47787  dfsclnbgr6  48349  aacllem  50291