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

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