ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpteq2dva Unicode version

Theorem mpteq2dva 3986
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
StepHypRef Expression
1 nfv 1491 . 2  |-  F/ x ph
2 mpteq2dva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
31, 2mpteq2da 3985 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1314    e. wcel 1463    |-> cmpt 3957
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-ral 2396  df-opab 3958  df-mpt 3959
This theorem is referenced by:  mpteq2dv  3987  fmptapd  5577  offval  5955  offval2  5963  caofinvl  5970  caofcom  5971  freceq1  6255  freceq2  6256  mapxpen  6708  xpmapenlem  6709  fser0const  10240  sumeq1  11075  sumeq2  11079  restid2  12035  cnmpt1t  12360  cnmpt12  12362  fsumcncntop  12631  divccncfap  12652  cdivcncfap  12662  expcncf  12667  dvidlemap  12735  dvcnp2cntop  12738  dvaddxxbr  12740  dvmulxxbr  12741  dvimulf  12745  dvcoapbr  12746  dvcjbr  12747  dvcj  12748  dvfre  12749  dvexp  12750  dvexp2  12751  dvrecap  12752  dvmptcmulcn  12758  dvmptnegcn  12759  dvmptsubcn  12760  dvef  12762
  Copyright terms: Public domain W3C validator