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  6087  rdgeq1  6374  rdgeq2  6375  omv  6458  oeiv  6459  0tonninf  10441  1tonninf  10442  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsum  10502  seq3f1olemp  10504  summodc  11393  zsumdc  11394  fsum3  11397  prodeq2w  11566  prodmodc  11588  zproddc  11589  fprodseq  11593  1arithlem1  12363  sloteq  12469  grplactfval  12976  cnprcl2k  13745  fsumcncntop  14095  expcncf  14131  dvexp  14214  dvexp2  14215  lgsval  14444  peano4nninf  14794  peano3nninf  14795  nninfalllem1  14796  nninfsellemdc  14798  nninfsellemeq  14802  nninfsellemqall  14803  nninfsellemeqinf  14804  nninfomni  14807