Theorem mpteq12dva 4483

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 1775	. 2 |- ( ph -> A. x A = C )
3		mpteq12dva.2	. . 3 |- ( ( ph /\ x e. A ) -> B = D )
4	3	ralrimiva 2804	. 2 |- ( ph -> A. x e. A B = D )
5		mpteq12f 4482	. 2 |- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
6	2, 4, 5	syl2anc 667	1 |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Syntax hints:   -> wi 4   /\ wa 371   A.wal 1444   = wceq 1446   e. wcel 1889   A.wral 2739   |-> cmpt 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2744  df-opab 4465  df-mpt 4466

This theorem is referenced by:  mpteq12dv  4484  reps  12880  repswccat  12895  cidpropd  15627  monpropd  15654  fucpropd  15894  curfpropd  16130  hofpropd  16164  yonffthlem  16179  ofco2  19488  pmatcollpw3fi1lem1  19822  rrxnm  22362  sgnsv  28502  ofcfval  28931  ccatmulgnn0dir  29440  signstf0  29469  cncfiooicc  37782  dvcosax  37808  fourierdlem74  38054  fourierdlem75  38055  fourierdlem93  38073  pfxmpt  38938  ushgredgedga  39316  ushgredgedgaloop  39318