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

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
StepHypRef Expression
1 mpteq12dv.1 . . 3  |-  ( ph  ->  A  =  C )
21alrimiv 1704 . 2  |-  ( ph  ->  A. x  A  =  C )
3 mpteq12dva.2 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
43ralrimiva 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 ) )
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 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
  Copyright terms: Public domain W3C validator