Theorem mpteq2da 4532

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 2467	. . 3 |- A = A
2	1	ax-gen 1601	. 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 434	. . 3 |- ( ph -> ( x e. A -> B = C ) )
6	3, 5	ralrimi 2864	. 2 |- ( ph -> A. x e. A B = C )
7		mpteq12f 4523	. 2 |- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
8	2, 6, 7	sylancr 663	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1377   = wceq 1379   F/wnf 1599   e. wcel 1767   A.wral 2814   |-> cmpt 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507

This theorem is referenced by:  mpteq2dva  4533  gsumsnfd  16769  gsummoncoe1  18117  cayleyhamilton1  19160  xkocnv  20050  utopsnneiplem  20485  offval2f  27178  fpwrelmap  27228  esumf1o  27701  prodeq1f  28617  prodeq2ii  28622  itg2addnclem  29643  ftc1anclem5  29671  mzpsubmpt  30279  mzpexpmpt  30281  refsum2cnlem1  30990  fmuldfeqlem1  31132  cncfiooicclem1  31232  stoweidlem2  31302  stoweidlem6  31306  stoweidlem8  31308  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem21  31321  stoweidlem22  31322  stoweidlem23  31323  stoweidlem32  31332  stoweidlem36  31336  stoweidlem40  31340  stoweidlem41  31341  stoweidlem47  31347  stirlinglem15  31388  gsumsndf  32018