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

Theorem mpteq12i 4537
Description: An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12i.1  |-  A  =  C
mpteq12i.2  |-  B  =  D
Assertion
Ref Expression
mpteq12i  |-  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D )

Proof of Theorem mpteq12i
StepHypRef Expression
1 mpteq12i.1 . . . 4  |-  A  =  C
21a1i 11 . . 3  |-  ( T. 
->  A  =  C
)
3 mpteq12i.2 . . . 4  |-  B  =  D
43a1i 11 . . 3  |-  ( T. 
->  B  =  D
)
52, 4mpteq12dv 4531 . 2  |-  ( T. 
->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
65trud 1388 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   T. wtru 1380    |-> cmpt 4511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2822  df-opab 4512  df-mpt 4513
This theorem is referenced by:  offres  6790  pmtrprfval  16385  dprdvalOLD  16909  evlsval  18058  madufval  19008  limcdif  22148  dfhnorm2  25862  cdj3lem3  27180  cdj3lem3b  27182  partfun  27339  esumsn  27897  measinb2  28019  eulerpart  28146  fiblem  28162  trlset  35358
  Copyright terms: Public domain W3C validator