Theorem mpteq12dva 4510

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)

Hypotheses

Ref	Expression
mpteq12dv.1	|- ( ph -> A = C )
mpteq12dva.2	|- ( ( ph /\ x e. A ) -> B = D )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)   D( x)

Proof of Theorem mpteq12dva

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. . 3 |- ( ph -> A = C )
2	1	alrimiv 1704	. 2 |- ( ph -> A. x A = C )
3		mpteq12dva.2	. . 3 |- ( ( ph /\ x e. A ) -> B = D )
4	3	ralrimiva 2855	. 2 |- ( ph -> A. x e. A B = D )
5		mpteq12f 4509	. 2 |- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
6	2, 4, 5	syl2anc 661	1 |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1379   = wceq 1381   e. wcel 1802   A.wral 2791   |-> cmpt 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-ral 2796  df-opab 4492  df-mpt 4493

This theorem is referenced by:  mpteq12dv  4511  reps  12716  repswccat  12731  cidpropd  14977  monpropd  15004  fucpropd  15215  curfpropd  15371  hofpropd  15405  yonffthlem  15420  ofco2  18820  pmatcollpw3fi1lem1  19154  rrxnm  21689  sgnsv  27583  ofcfval  27963  ccatmulgnn0dir  28362  signstf0  28391  cncfiooicc  31600  dvcosax  31623  fourierdlem74  31848  fourierdlem75  31849  fourierdlem93  31867