Theorem mpteq2dv 4175

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   |-> cmpt 4145

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-ral 2513  df-opab 4146  df-mpt 4147

This theorem is referenced by:  ofeqd  6226  ofeq  6227  rdgeq1  6523  rdgeq2  6524  omv  6609  oeiv  6610  0tonninf  10674  1tonninf  10675  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seq3f1olemp  10749  summodc  11910  zsumdc  11911  fsum3  11914  prodeq2w  12083  prodmodc  12105  zproddc  12106  fprodseq  12110  nninfctlemfo  12577  1arithlem1  12902  sloteq  13053  prdsplusgval  13332  prdsmulrval  13334  qusex  13374  grplactfval  13650  cnprcl2k  14896  fsumcncntop  15257  expcn  15259  expcncf  15299  dvexp  15401  dvexp2  15402  dvmptfsum  15415  elply2  15425  elplyr  15430  elplyd  15431  plycolemc  15448  dvply2g  15456  lgsval  15699  incistruhgr  15906  peano4nninf  16460  peano3nninf  16461  nninfalllem1  16462  nninfsellemdc  16464  nninfsellemeq  16468  nninfsellemqall  16469  nninfsellemeqinf  16470  nninfomni  16473  nnnninfex  16476