Theorem mpteq2dv 4096

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148   |-> cmpt 4066

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-opab 4067  df-mpt 4068

This theorem is referenced by:  ofeq  6088  rdgeq1  6375  rdgeq2  6376  omv  6459  oeiv  6460  0tonninf  10442  1tonninf  10443  iseqf1olemjpcl  10498  iseqf1olemqpcl  10499  iseqf1olemfvp  10500  seq3f1olemqsum  10503  seq3f1olemp  10505  summodc  11394  zsumdc  11395  fsum3  11398  prodeq2w  11567  prodmodc  11589  zproddc  11590  fprodseq  11594  1arithlem1  12364  sloteq  12470  qusex  12752  grplactfval  12978  cnprcl2k  13867  fsumcncntop  14217  expcncf  14253  dvexp  14336  dvexp2  14337  lgsval  14566  peano4nninf  14917  peano3nninf  14918  nninfalllem1  14919  nninfsellemdc  14921  nninfsellemeq  14925  nninfsellemqall  14926  nninfsellemeqinf  14927  nninfomni  14930