Theorem mpteq2dv 4121

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 4120	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164   |-> cmpt 4091

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-ral 2477  df-opab 4092  df-mpt 4093

This theorem is referenced by:  ofeqd  6134  ofeq  6135  rdgeq1  6426  rdgeq2  6427  omv  6510  oeiv  6511  0tonninf  10514  1tonninf  10515  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsum  10587  seq3f1olemp  10589  summodc  11529  zsumdc  11530  fsum3  11533  prodeq2w  11702  prodmodc  11724  zproddc  11725  fprodseq  11729  nninfctlemfo  12180  1arithlem1  12504  sloteq  12626  qusex  12911  grplactfval  13176  cnprcl2k  14385  fsumcncntop  14746  expcn  14748  expcncf  14788  dvexp  14890  dvexp2  14891  dvmptfsum  14904  elply2  14914  elplyr  14919  elplyd  14920  plycolemc  14936  lgsval  15161  peano4nninf  15566  peano3nninf  15567  nninfalllem1  15568  nninfsellemdc  15570  nninfsellemeq  15574  nninfsellemqall  15575  nninfsellemeqinf  15576  nninfomni  15579