Theorem mpteq2dv 4224

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209   |-> cmpt 4193

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-opab 4194  df-mpt 4195

This theorem is used by:  ofeqd  6307  ofeq  6308  rdgeq1  6646  rdgeq2  6647  omv  6732  oeiv  6733  indval  9305  0tonninf  10898  1tonninf  10899  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsum  10971  seq3f1olemp  10973  summodc  12175  zsumdc  12176  fsum3  12179  prodeq2w  12348  prodmodc  12370  zproddc  12371  fprodseq  12375  nninfctlemfo  12842  1arithlem1  13171  ballotfilemfval  13287  ballotfi  13340  sloteq  13415  qusex  13705  grplactfval  13965  gsumsncmn  14246  prdsplusgval  14290  prdsmulrval  14292  psrmulfval  15187  cnprcl2k  15432  fsumcncntop  15793  expcn  15795  expcncf  15835  dvexp  15937  dvexp2  15938  dvmptfsum  15951  elply2  15961  elplyr  15966  elplyd  15967  plycolemc  15984  dvply2g  15992  lgsval  16328  incistruhgr  16536  peano4nninf  17255  peano3nninf  17256  nninfalllem1  17257  nninfsellemdc  17259  nninfsellemeq  17263  nninfsellemqall  17264  nninfsellemeqinf  17265  nninfomni  17268  nnnninfex  17271