Theorem mpteq2dv 4135

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)

Hypothesis

Ref	Expression
mpteq2dv.1	|- ( ph -> B = C )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 |- ( ph -> B = C )
2	1	adantr 276	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 4134	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = 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:  ofeqd  6160  ofeq  6161  rdgeq1  6457  rdgeq2  6458  omv  6541  oeiv  6542  0tonninf  10585  1tonninf  10586  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsum  10658  seq3f1olemp  10660  summodc  11694  zsumdc  11695  fsum3  11698  prodeq2w  11867  prodmodc  11889  zproddc  11890  fprodseq  11894  nninfctlemfo  12361  1arithlem1  12686  sloteq  12837  prdsplusgval  13115  prdsmulrval  13117  qusex  13157  grplactfval  13433  cnprcl2k  14678  fsumcncntop  15039  expcn  15041  expcncf  15081  dvexp  15183  dvexp2  15184  dvmptfsum  15197  elply2  15207  elplyr  15212  elplyd  15213  plycolemc  15230  dvply2g  15238  lgsval  15481  peano4nninf  15943  peano3nninf  15944  nninfalllem1  15945  nninfsellemdc  15947  nninfsellemeq  15951  nninfsellemqall  15952  nninfsellemeqinf  15953  nninfomni  15956  nnnninfex  15959