Theorem mpteq2da 5162

Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)

Hypotheses

Ref	Expression
mpteq2da.1	⊢ Ⅎ𝑥𝜑
mpteq2da.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2da	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Proof of Theorem mpteq2da

Step	Hyp	Ref	Expression
1		eqid 2823	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1796	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2da.1	. . 3 ⊢ Ⅎ𝑥𝜑
4		mpteq2da.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
5	4	ex 415	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶))
6	3, 5	ralrimi 3218	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
7		mpteq12f 5151	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
8	2, 6, 7	sylancr 589	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1535   = wceq 1537  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3140   ↦ cmpt 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-opab 5131  df-mpt 5149

This theorem is referenced by:  mpteq2dva  5163  offval2f  7423  prodeq1f  15264  prodeq2ii  15269  gsumsnfd  19073  gsummoncoe1  20474  cayleyhamilton1  21502  xkocnv  22424  utopsnneiplem  22858  fpwrelmap  30471  gsummpt2d  30689  fedgmullem2  31028  esumf1o  31311  esum2d  31354  itg2addnclem  34945  ftc1anclem5  34973  mzpsubmpt  39347  mzpexpmpt  39349  refsum2cnlem1  41301  fmuldfeqlem1  41870  limsupval3  41980  liminfval5  42053  liminfvalxrmpt  42074  liminfval4  42077  limsupval4  42082  liminfvaluz2  42083  limsupvaluz4  42088  cncfiooicclem1  42183  dvmptfprodlem  42236  stoweidlem2  42294  stoweidlem6  42298  stoweidlem8  42300  stoweidlem17  42309  stoweidlem19  42311  stoweidlem20  42312  stoweidlem21  42313  stoweidlem22  42314  stoweidlem23  42315  stoweidlem32  42324  stoweidlem36  42328  stoweidlem40  42332  stoweidlem41  42333  stoweidlem47  42339  stirlinglem15  42380  sge0ss  42701  sge0xp  42718  omeiunlempt  42809  hoicvrrex  42845  ovnlecvr2  42899  smfdiv  43079  smfneg  43085  smflimmpt  43091  smfsupmpt  43096  smfinfmpt  43100  smflimsuplem4  43104  smflimsuplem5  43105  smflimsupmpt  43110  smfliminf  43112  smfliminfmpt  43113