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  6647  rdgeq2  6648  omv  6733  oeiv  6734  indval  9305  0tonninf  10897  1tonninf  10898  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsum  10970  seq3f1olemp  10972  summodc  12174  zsumdc  12175  fsum3  12178  prodeq2w  12347  prodmodc  12369  zproddc  12370  fprodseq  12374  nninfctlemfo  12841  1arithlem1  13170  ballotfilemfval  13286  ballotfi  13339  sloteq  13414  qusex  13704  grplactfval  13964  gsumsncmn  14245  prdsplusgval  14289  prdsmulrval  14291  psrmulfval  15196  mvrval  15215  cnprcl2k  15449  fsumcncntop  15810  expcn  15812  expcncf  15852  dvexp  15954  dvexp2  15955  dvmptfsum  15968  elply2  15978  elplyr  15983  elplyd  15984  plycolemc  16001  dvply2g  16009  lgsval  16345  incistruhgr  16553  peano4nninf  17272  peano3nninf  17273  nninfalllem1  17274  nninfsellemdc  17276  nninfsellemeq  17280  nninfsellemqall  17281  nninfsellemeqinf  17282  nninfomni  17285  nnnninfex  17288