Theorem mpteq2i 4131

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpteq2i.1	|- B = C

Assertion

Ref	Expression
mpteq2i	|- ( x e. A |-> B ) = ( x e. A |-> C )

Proof of Theorem mpteq2i

Step	Hyp	Ref	Expression
1		mpteq2i.1	. . 3 |- B = C
2	1	a1i 9	. 2 |- ( x e. A -> B = C )
3	2	mpteq2ia 4130	1 |- ( x e. A |-> B ) = ( x e. A |-> C )

Syntax hints:   = wceq 1373   e. wcel 2176   |-> cmpt 4105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-ral 2489  df-opab 4106  df-mpt 4107

This theorem is referenced by:  frecsuc  6493  fodjuomni  7251  fodjumkv  7262  axcaucvg  8013  0tonninf  10585  1tonninf  10586  cbvsum  11671  cbvprod  11869  eirraplem  12088  znzrh2  14408  cnmpt12f  14758  fsumcncntop  15039  dvmptfsum  15197  dvef  15199  plyco  15231  plycj  15233  nninfsellemqall  15952  nninfomni  15956  nnnninfex  15959  exmidsbthr  15962