Theorem mpteq2dv 4142

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177   ↦ cmpt 4112

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-ral 2490  df-opab 4113  df-mpt 4114

This theorem is referenced by:  ofeqd  6172  ofeq  6173  rdgeq1  6469  rdgeq2  6470  omv  6553  oeiv  6554  0tonninf  10602  1tonninf  10603  iseqf1olemjpcl  10670  iseqf1olemqpcl  10671  iseqf1olemfvp  10672  seq3f1olemqsum  10675  seq3f1olemp  10677  summodc  11764  zsumdc  11765  fsum3  11768  prodeq2w  11937  prodmodc  11959  zproddc  11960  fprodseq  11964  nninfctlemfo  12431  1arithlem1  12756  sloteq  12907  prdsplusgval  13185  prdsmulrval  13187  qusex  13227  grplactfval  13503  cnprcl2k  14748  fsumcncntop  15109  expcn  15111  expcncf  15151  dvexp  15253  dvexp2  15254  dvmptfsum  15267  elply2  15277  elplyr  15282  elplyd  15283  plycolemc  15300  dvply2g  15308  lgsval  15551  incistruhgr  15756  peano4nninf  16078  peano3nninf  16079  nninfalllem1  16080  nninfsellemdc  16082  nninfsellemeq  16086  nninfsellemqall  16087  nninfsellemeqinf  16088  nninfomni  16091  nnnninfex  16094