Theorem mpteq2dv 4217

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 4216	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209   ↦ cmpt 4187

This theorem was proved from 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 theorem 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 4188  df-mpt 4189

This theorem is referenced by:  ofeqd  6294  ofeq  6295  rdgeq1  6632  rdgeq2  6633  omv  6718  oeiv  6719  0tonninf  10855  1tonninf  10856  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsum  10928  seq3f1olemp  10930  summodc  12128  zsumdc  12129  fsum3  12132  prodeq2w  12301  prodmodc  12323  zproddc  12324  fprodseq  12328  nninfctlemfo  12795  1arithlem1  13120  ballotfilemfval  13207  ballotfi  13260  sloteq  13335  qusex  13623  grplactfval  13883  gsumsncmn  14133  prdsplusgval  14160  prdsmulrval  14162  cnprcl2k  15230  fsumcncntop  15591  expcn  15593  expcncf  15633  dvexp  15735  dvexp2  15736  dvmptfsum  15749  elply2  15759  elplyr  15764  elplyd  15765  plycolemc  15782  dvply2g  15790  lgsval  16037  incistruhgr  16245  peano4nninf  16954  peano3nninf  16955  nninfalllem1  16956  nninfsellemdc  16958  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  nninfomni  16967  nnnninfex  16970