Theorem mpteq2dv 3951

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 271	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 3950	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1296   e. wcel 1445   |-> cmpt 3921

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-ral 2375  df-opab 3922  df-mpt 3923

This theorem is referenced by:  ofeq  5896  rdgeq1  6174  rdgeq2  6175  omv  6256  oeiv  6257  0tonninf  9994  1tonninf  9995  iseqf1olemjpcl  10061  iseqf1olemqpcl  10062  iseqf1olemfvp  10063  seq3f1olemqsum  10066  seq3f1olemp  10068  summodc  10941  zsumdc  10942  fsum3  10945  sloteq  11663  cnprcl2k  12072  peano4nninf  12605  peano3nninf  12606  nninfalllem1  12608  nninfsellemdc  12611  nninfsellemeq  12615  nninfsellemqall  12616  nninfsellemeqinf  12617  nninfomni  12620