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  9296  0tonninf  10877  1tonninf  10878  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsum  10950  seq3f1olemp  10952  summodc  12150  zsumdc  12151  fsum3  12154  prodeq2w  12323  prodmodc  12345  zproddc  12346  fprodseq  12350  nninfctlemfo  12817  1arithlem1  13142  ballotfilemfval  13229  ballotfi  13282  sloteq  13357  qusex  13646  grplactfval  13906  gsumsncmn  14156  prdsplusgval  14183  prdsmulrval  14185  cnprcl2k  15307  fsumcncntop  15668  expcn  15670  expcncf  15710  dvexp  15812  dvexp2  15813  dvmptfsum  15826  elply2  15836  elplyr  15841  elplyd  15842  plycolemc  15859  dvply2g  15867  lgsval  16127  incistruhgr  16335  peano4nninf  17053  peano3nninf  17054  nninfalllem1  17055  nninfsellemdc  17057  nninfsellemeq  17061  nninfsellemqall  17062  nninfsellemeqinf  17063  nninfomni  17066  nnnninfex  17069