Theorem mpteq2da 4461

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 2450	. . 3 |- A = A
2	1	ax-gen 1592	. 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 2879	. 2 |- ( ph -> A. x e. A B = C )
7		mpteq12f 4452	. 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 1368   = wceq 1370   F/wnf 1590   e. wcel 1757   A.wral 2792   |-> cmpt 4434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-ral 2797  df-opab 4435  df-mpt 4436

This theorem is referenced by:  mpteq2dva  4462  xkocnv  19489  utopsnneiplem  19924  offval2f  26103  fpwrelmap  26153  esumf1o  26624  prodeq1f  27541  prodeq2ii  27546  itg2addnclem  28567  ftc1anclem5  28595  mzpsubmpt  29203  mzpexpmpt  29205  refsum2cnlem1  29883  fmuldfeqlem1  29887  stoweidlem2  29921  stoweidlem6  29925  stoweidlem8  29927  stoweidlem17  29936  stoweidlem19  29938  stoweidlem20  29939  stoweidlem21  29940  stoweidlem22  29941  stoweidlem23  29942  stoweidlem32  29951  stoweidlem36  29955  stoweidlem40  29959  stoweidlem41  29960  stoweidlem47  29966  stirlinglem15  30007  gsumsndf  30887  gsummoncoe1  30971  cayleyhamilton1  31333