Theorem uneq1d 3766

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

Syntax hints:   → wi 4   = wceq 1483   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  ifeq1  4090  preq1  4268  tpeq1  4277  tpeq2  4278  tpprceq3  4335  iunxdif3  4606  iununi  4610  resasplit  6074  fresaunres2  6076  fmptpr  6438  funresdfunsn  6455  ressuppssdif  7316  sbthlem5  8074  fodomr  8111  domunfican  8233  brwdom2  8478  cdaval  8992  ackbij1lem2  9043  ttukeylem3  9333  snunioo  12298  snunioc  12300  prunioo  12301  fzpred  12389  fseq1p1m1  12414  nn0split  12454  fz0sn0fz1  12456  fzo0sn0fzo1  12557  fzosplitpr  12577  s2prop  13652  s4prop  13655  fsum1p  14482  fprod1p  14698  setsval  15888  setsabs  15902  setscom  15903  prdsval  16115  prdsdsval  16138  prdsdsval2  16144  prdsdsval3  16145  mreexexlem3d  16306  mreexexlem4d  16307  estrres  16779  symg2bas  17818  evlseu  19516  ordtuni  20994  lfinun  21328  alexsubALTlem3  21853  ustssco  22018  trust  22033  ressprdsds  22176  xpsdsval  22186  nulmbl2  23304  uniioombllem3  23353  uniioombllem4  23354  plyeq0  23967  plyaddlem1  23969  plymullem1  23970  fta1lem  24062  vieta1lem2  24066  birthdaylem2  24679  edglnl  26038  iuninc  29379  difelcarsg  30372  actfunsnf1o  30682  reprsuc  30693  breprexplema  30708  bnj1416  31107  mclsval  31460  mclsax  31466  rankung  32273  topjoin  32360  bj-tageq  32964  finixpnum  33394  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem16  33425  poimirlem17  33426  poimirlem28  33437  mblfinlem2  33447  islshpsm  34267  lshpnel2N  34272  lkrlsp3  34391  pclfinclN  35236  dochsatshp  36740  mapfzcons1  37280  iunrelexp0  37994  isotone1  38346  fiiuncl  39234  nnsplit  39574  fourierdlem32  40356  fzopred  41332  fzopredsuc  41333  aacllem  42547