Theorem mpteq2dv 4174

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200   ↦ cmpt 4144

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-ral 2513  df-opab 4145  df-mpt 4146

This theorem is referenced by:  ofeqd  6218  ofeq  6219  rdgeq1  6515  rdgeq2  6516  omv  6599  oeiv  6600  0tonninf  10657  1tonninf  10658  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsum  10730  seq3f1olemp  10732  summodc  11889  zsumdc  11890  fsum3  11893  prodeq2w  12062  prodmodc  12084  zproddc  12085  fprodseq  12089  nninfctlemfo  12556  1arithlem1  12881  sloteq  13032  prdsplusgval  13311  prdsmulrval  13313  qusex  13353  grplactfval  13629  cnprcl2k  14874  fsumcncntop  15235  expcn  15237  expcncf  15277  dvexp  15379  dvexp2  15380  dvmptfsum  15393  elply2  15403  elplyr  15408  elplyd  15409  plycolemc  15426  dvply2g  15434  lgsval  15677  incistruhgr  15884  peano4nninf  16331  peano3nninf  16332  nninfalllem1  16333  nninfsellemdc  16335  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfomni  16344  nnnninfex  16347