Theorem mpteq2dv 3977

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 272	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 3976	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1312   ∈ wcel 1461   ↦ cmpt 3947

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-ral 2393  df-opab 3948  df-mpt 3949

This theorem is referenced by:  ofeq  5936  rdgeq1  6219  rdgeq2  6220  omv  6302  oeiv  6303  0tonninf  10098  1tonninf  10099  iseqf1olemjpcl  10154  iseqf1olemqpcl  10155  iseqf1olemfvp  10156  seq3f1olemqsum  10159  seq3f1olemp  10161  summodc  11037  zsumdc  11038  fsum3  11041  sloteq  11800  cnprcl2k  12210  fsumcncntop  12535  expcncf  12571  peano4nninf  12877  peano3nninf  12878  nninfalllem1  12880  nninfsellemdc  12883  nninfsellemeq  12887  nninfsellemqall  12888  nninfsellemeqinf  12889  nninfomni  12892