Theorem mpteq2dv 4222

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)

Hypothesis

Ref	Expression
mpteq2dv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dv	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 4221	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209   ↦ cmpt 4192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-opab 4193  df-mpt 4194

This theorem is used by:  ofeqd  6304  ofeq  6305  rdgeq1  6642  rdgeq2  6643  omv  6728  oeiv  6729  indval  9298  0tonninf  10890  1tonninf  10891  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsum  10963  seq3f1olemp  10965  summodc  12166  zsumdc  12167  fsum3  12170  prodeq2w  12339  prodmodc  12361  zproddc  12362  fprodseq  12366  nninfctlemfo  12833  1arithlem1  13162  ballotfilemfval  13278  ballotfi  13331  sloteq  13406  qusex  13695  grplactfval  13955  gsumsncmn  14205  prdsplusgval  14232  prdsmulrval  14234  cnprcl2k  15356  fsumcncntop  15717  expcn  15719  expcncf  15759  dvexp  15861  dvexp2  15862  dvmptfsum  15875  elply2  15885  elplyr  15890  elplyd  15891  plycolemc  15908  dvply2g  15916  lgsval  16221  incistruhgr  16429  peano4nninf  17147  peano3nninf  17148  nninfalllem1  17149  nninfsellemdc  17151  nninfsellemeq  17155  nninfsellemqall  17156  nninfsellemeqinf  17157  nninfomni  17160  nnnninfex  17163