Theorem mpteq2dv 4125

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167   |-> cmpt 4095

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-opab 4096  df-mpt 4097

This theorem is referenced by:  ofeqd  6141  ofeq  6142  rdgeq1  6438  rdgeq2  6439  omv  6522  oeiv  6523  0tonninf  10549  1tonninf  10550  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsum  10622  seq3f1olemp  10624  summodc  11565  zsumdc  11566  fsum3  11569  prodeq2w  11738  prodmodc  11760  zproddc  11761  fprodseq  11765  nninfctlemfo  12232  1arithlem1  12557  sloteq  12708  prdsplusgval  12985  prdsmulrval  12987  qusex  13027  grplactfval  13303  cnprcl2k  14526  fsumcncntop  14887  expcn  14889  expcncf  14929  dvexp  15031  dvexp2  15032  dvmptfsum  15045  elply2  15055  elplyr  15060  elplyd  15061  plycolemc  15078  dvply2g  15086  lgsval  15329  peano4nninf  15737  peano3nninf  15738  nninfalllem1  15739  nninfsellemdc  15741  nninfsellemeq  15745  nninfsellemqall  15746  nninfsellemeqinf  15747  nninfomni  15750