Theorem mpteq2dv 4201

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203   ↦ cmpt 4171

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-ral 2525  df-opab 4172  df-mpt 4173

This theorem is referenced by:  ofeqd  6268  ofeq  6269  rdgeq1  6602  rdgeq2  6603  omv  6688  oeiv  6689  0tonninf  10802  1tonninf  10803  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsum  10875  seq3f1olemp  10877  summodc  12069  zsumdc  12070  fsum3  12073  prodeq2w  12242  prodmodc  12264  zproddc  12265  fprodseq  12269  nninfctlemfo  12736  1arithlem1  13061  sloteq  13217  prdsplusgval  13496  prdsmulrval  13498  qusex  13538  grplactfval  13814  cnprcl2k  15071  fsumcncntop  15432  expcn  15434  expcncf  15474  dvexp  15576  dvexp2  15577  dvmptfsum  15590  elply2  15600  elplyr  15605  elplyd  15606  plycolemc  15623  dvply2g  15631  lgsval  15877  incistruhgr  16085  peano4nninf  16784  peano3nninf  16785  nninfalllem1  16786  nninfsellemdc  16788  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  nninfomni  16797  nnnninfex  16800  gfsumsn  16867