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  9299  0tonninf  10892  1tonninf  10893  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsum  10965  seq3f1olemp  10967  summodc  12169  zsumdc  12170  fsum3  12173  prodeq2w  12342  prodmodc  12364  zproddc  12365  fprodseq  12369  nninfctlemfo  12836  1arithlem1  13165  ballotfilemfval  13281  ballotfi  13334  sloteq  13409  qusex  13699  grplactfval  13959  gsumsncmn  14240  prdsplusgval  14267  prdsmulrval  14269  psrmulfval  15159  cnprcl2k  15398  fsumcncntop  15759  expcn  15761  expcncf  15801  dvexp  15903  dvexp2  15904  dvmptfsum  15917  elply2  15927  elplyr  15932  elplyd  15933  plycolemc  15950  dvply2g  15958  lgsval  16289  incistruhgr  16497  peano4nninf  17215  peano3nninf  17216  nninfalllem1  17217  nninfsellemdc  17219  nninfsellemeq  17223  nninfsellemqall  17224  nninfsellemeqinf  17225  nninfomni  17228  nnnninfex  17231