Theorem mpteq2dv 4089

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2146   ↦ cmpt 4059

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-ral 2458  df-opab 4060  df-mpt 4061

This theorem is referenced by:  ofeq  6075  rdgeq1  6362  rdgeq2  6363  omv  6446  oeiv  6447  0tonninf  10407  1tonninf  10408  iseqf1olemjpcl  10463  iseqf1olemqpcl  10464  iseqf1olemfvp  10465  seq3f1olemqsum  10468  seq3f1olemp  10470  summodc  11357  zsumdc  11358  fsum3  11361  prodeq2w  11530  prodmodc  11552  zproddc  11553  fprodseq  11557  1arithlem1  12326  sloteq  12432  grplactfval  12830  cnprcl2k  13275  fsumcncntop  13625  expcncf  13661  dvexp  13744  dvexp2  13745  lgsval  13974  peano4nninf  14314  peano3nninf  14315  nninfalllem1  14316  nninfsellemdc  14318  nninfsellemeq  14322  nninfsellemqall  14323  nninfsellemeqinf  14324  nninfomni  14327