Theorem mpteq2dva 4077

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)

Hypothesis

Ref	Expression
mpteq2dva.1	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

Ref	Expression
mpteq2dva	|- ( 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 mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1521	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4076	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   e. wcel 2141   |-> cmpt 4048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-ral 2453  df-opab 4049  df-mpt 4050

This theorem is referenced by:  mpteq2dv  4078  fmptapd  5684  offval  6065  offval2  6073  caofinvl  6080  caofcom  6081  freceq1  6368  freceq2  6369  mapxpen  6822  xpmapenlem  6823  nnnninf2  7099  fser0const  10459  sumeq1  11305  sumeq2  11309  prodeq2  11507  prod1dc  11536  restid2  12574  cnmpt1t  13000  cnmpt12  13002  fsumcncntop  13271  divccncfap  13292  cdivcncfap  13302  expcncf  13307  dvidlemap  13375  dvcnp2cntop  13378  dvaddxxbr  13380  dvmulxxbr  13381  dvimulf  13385  dvcoapbr  13386  dvcjbr  13387  dvcj  13388  dvfre  13389  dvexp  13390  dvexp2  13391  dvrecap  13392  dvmptcmulcn  13398  dvmptnegcn  13399  dvmptsubcn  13400  dvef  13403  lgsval4lem  13627  lgsneg  13640  lgsmod  13642