Theorem uneq1d 4121

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  ifeq1  4485  preq1  4692  tpeq1  4701  tpeq2  4702  tpprceq3  4762  iunxdif3  5052  iununi  5056  resasplit  6712  fresaunres2  6714  fmptpr  7128  funresdfunsn  7145  ressuppssdif  8137  on2recsov  8606  sbthlem5  9031  fodomr  9068  domunfican  9234  fodomfir  9240  brwdom2  9490  ackbij1lem2  10142  ttukeylem3  10433  snunioo  13406  snunioc  13408  prunioo  13409  fzpred  13500  fseq1p1m1  13526  nn0split  13571  fz0sn0fz1  13573  fzo0sn0fzo1  13683  fzosplitpr  13705  s2prop  14842  s4prop  14845  fsum1p  15688  fprod1p  15903  setsval  17106  setsabs  17118  setscom  17119  prdsval  17387  prdsdsval  17410  prdsdsval2  17416  prdsdsval3  17417  mreexexlem3d  17581  mreexexlem4d  17582  estrres  18074  symg2bas  19334  symgvalstruct  19338  evlseu  22050  ordtuni  23146  lfinun  23481  alexsubALTlem3  24005  ustssco  24171  trust  24185  ressprdsds  24327  xpsdsval  24337  nulmbl2  25505  uniioombllem3  25554  uniioombllem4  25555  plyeq0  26184  plyaddlem1  26186  plymullem1  26187  fta1lem  26283  vieta1lem2  26287  birthdaylem2  26930  noetasuplem2  27714  noxpordpred  27961  addsproplem1  27977  addsprop  27984  negsproplem1  28036  negsprop  28043  mulsproplemcbv  28123  mulsproplem1  28124  mulsprop  28138  precsexlemcbv  28214  precsexlem3  28217  edglnl  29228  iuninc  32646  nn0diffz0  32884  pmtrcnel2  33183  tocycval  33201  cycpmco2rn  33218  evlextv  33718  difelcarsg  34487  actfunsnf1o  34781  reprsuc  34792  breprexplema  34807  bnj1416  35214  mclsval  35776  mclsax  35782  rankung  36379  topjoin  36578  bj-tageq  37221  finixpnum  37853  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem9  37877  poimirlem16  37884  poimirlem17  37885  poimirlem28  37896  mblfinlem2  37906  islshpsm  39353  lshpnel2N  39358  lkrlsp3  39477  pclfinclN  40323  dochsatshp  41824  mapfzcons1  43071  iunrelexp0  44055  isotone1  44401  fiiuncl  45422  nnsplit  45714  fourierdlem32  46494  fzopred  47679  fzopredsuc  47680  dfsclnbgr6  48215  aacllem  50157