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

Theorem ffnd 5243
Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
ffnd.1  |-  ( ph  ->  F : A --> B )
Assertion
Ref Expression
ffnd  |-  ( ph  ->  F  Fn  A )

Proof of Theorem ffnd
StepHypRef Expression
1 ffnd.1 . 2  |-  ( ph  ->  F : A --> B )
2 ffn 5242 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 14 1  |-  ( ph  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5088   -->wf 5089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f 5097
This theorem is referenced by:  offeq  5963  difinfsn  6953  ctssdc  6966  seqvalcd  10200  seq3feq2  10211  seq3feq  10213  seqfeq3  10253  ser0f  10256  facnn  10441  fac0  10442  resunimafz0  10542  seq3shft  10578  fisumss  11129  efcvgfsum  11300  ennnfonelemfun  11857  ennnfonelemf1  11858  cnrest2  12332  lmss  12342  lmtopcnp  12346  upxp  12368  uptx  12370  cnmpt11  12379  cnmpt21  12387  cnmpt22f  12391  cnmptcom  12394  hmeof1o2  12404  psmetxrge0  12428  isxmet2d  12444  blelrnps  12515  blelrn  12516  xmetresbl  12536  comet  12595  bdxmet  12597  xmettx  12606  dvidlemap  12756  dvaddxxbr  12761  dvmulxxbr  12762  dvrecap  12773  nninfalllemn  13129  nninfall  13131  nninfsellemeqinf  13139  nninffeq  13143  refeq  13150
  Copyright terms: Public domain W3C validator