Theorem mpteq12i 4742

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

Step	Hyp	Ref	Expression
1		mpteq12i.1	. . . 4 |- A = C
2	1	a1i 11	. . 3 |- ( T. -> A = C )
3		mpteq12i.2	. . . 4 |- B = D
4	3	a1i 11	. . 3 |- ( T. -> B = D )
5	2, 4	mpteq12dv 4733	. 2 |- ( T. -> ( x e. A |-> B ) = ( x e. C |-> D ) )
6	5	trud 1493	1 |- ( x e. A |-> B ) = ( x e. C |-> D )

Syntax hints:   = wceq 1483   T. wtru 1484   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  offres  7163  pmtrprfval  17907  evlsval  19519  madufval  20443  limcdif  23640  dfhnorm2  27979  cdj3lem3  29297  cdj3lem3b  29299  partfun  29475  esumsnf  30126  esumrnmpt2  30130  measinb2  30286  eulerpart  30444  fiblem  30460  trlset  35448  hoidmvlelem4  40812  smflimsup  41034