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

Theorem mpteq12i 4487
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 4481 . 2  |-  ( T. 
->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
65trud 1379 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   T. wtru 1371    |-> cmpt 4461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2804  df-opab 4462  df-mpt 4463
This theorem is referenced by:  offres  6685  pmtrprfval  16116  dprdvalOLD  16619  evlsval  17739  madufval  18585  limcdif  21494  dfhnorm2  24703  cdj3lem3  26021  cdj3lem3b  26023  partfun  26171  esumsn  26683  measinb2  26805  eulerpart  26932  fiblem  26948  trlset  34168
  Copyright terms: Public domain W3C validator