Theorem mpteq12dva 4534

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 1720	. 2 |- ( ph -> A. x A = C )
3		mpteq12dva.2	. . 3 |- ( ( ph /\ x e. A ) -> B = D )
4	3	ralrimiva 2871	. 2 |- ( ph -> A. x e. A B = D )
5		mpteq12f 4533	. 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 1393   = wceq 1395   e. wcel 1819   A.wral 2807   |-> cmpt 4515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4516  df-mpt 4517

This theorem is referenced by:  mpteq12dv  4535  reps  12754  repswccat  12769  cidpropd  15126  monpropd  15153  fucpropd  15393  curfpropd  15629  hofpropd  15663  yonffthlem  15678  ofco2  19080  pmatcollpw3fi1lem1  19414  rrxnm  21949  sgnsv  27877  ofcfval  28270  ccatmulgnn0dir  28693  signstf0  28722  cncfiooicc  31900  dvcosax  31926  fourierdlem74  32166  fourierdlem75  32167  fourierdlem93  32185  pfxmpt  32504