MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq12dva Structured version   Unicode version

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
StepHypRef Expression
1 mpteq12dv.1 . . 3  |-  ( ph  ->  A  =  C )
21alrimiv 1720 . 2  |-  ( ph  ->  A. x  A  =  C )
3 mpteq12dva.2 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
43ralrimiva 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 ) )
62, 4, 5syl2anc 661 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator