Theorem mpteq2da 4524

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	|- F/ x ph
mpteq2da.2	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

Ref	Expression
mpteq2da	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Proof of Theorem mpteq2da

Step	Hyp	Ref	Expression
1		eqid 2454	. . 3 |- A = A
2	1	ax-gen 1623	. 2 |- A. x A = A
3		mpteq2da.1	. . 3 |- F/ x ph
4		mpteq2da.2	. . . 4 |- ( ( ph /\ x e. A ) -> B = C )
5	4	ex 432	. . 3 |- ( ph -> ( x e. A -> B = C ) )
6	3, 5	ralrimi 2854	. 2 |- ( ph -> A. x e. A B = C )
7		mpteq12f 4515	. 2 |- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
8	2, 6, 7	sylancr 661	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 367   A.wal 1396   = wceq 1398   F/wnf 1621   e. wcel 1823   A.wral 2804   |-> cmpt 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-opab 4498  df-mpt 4499

This theorem is referenced by:  mpteq2dva  4525  prodeq1f  13800  prodeq2ii  13805  gsumsnfd  17177  gsummoncoe1  18544  cayleyhamilton1  19563  xkocnv  20484  utopsnneiplem  20919  offval2f  27736  fpwrelmap  27790  gsummpt2d  28009  esumf1o  28282  esum2d  28325  itg2addnclem  30309  ftc1anclem5  30337  mzpsubmpt  30918  mzpexpmpt  30920  refsum2cnlem1  31655  fmuldfeqlem1  31818  cncfiooicclem1  31938  dvmptfprodlem  31983  stoweidlem2  32026  stoweidlem6  32030  stoweidlem8  32032  stoweidlem17  32041  stoweidlem19  32043  stoweidlem20  32044  stoweidlem21  32045  stoweidlem22  32046  stoweidlem23  32047  stoweidlem32  32056  stoweidlem36  32060  stoweidlem40  32064  stoweidlem41  32065  stoweidlem47  32071  stirlinglem15  32112