Theorem mpteq2dva 4095

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 1528	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4094	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 104   = 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:  mpteq2dv  4096  fmptapd  5710  offval  6093  offval2  6101  caofinvl  6108  caofcom  6109  freceq1  6396  freceq2  6397  mapxpen  6851  xpmapenlem  6852  nnnninf2  7128  nninfwlpoimlemginf  7177  fser0const  10519  sumeq1  11366  sumeq2  11370  prodeq2  11568  prod1dc  11597  restid2  12703  qusin  12753  grpinvpropdg  12952  cnmpt1t  13946  cnmpt12  13948  fsumcncntop  14217  divccncfap  14238  cdivcncfap  14248  expcncf  14253  dvidlemap  14321  dvcnp2cntop  14324  dvaddxxbr  14326  dvmulxxbr  14327  dvimulf  14331  dvcoapbr  14332  dvcjbr  14333  dvcj  14334  dvfre  14335  dvexp  14336  dvexp2  14337  dvrecap  14338  dvmptcmulcn  14344  dvmptnegcn  14345  dvmptsubcn  14346  dvef  14349  lgsval4lem  14573  lgsneg  14586  lgsmod  14588