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

Theorem ffnd 5385
Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
ffnd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
ffnd (𝜑𝐹 Fn 𝐴)

Proof of Theorem ffnd
StepHypRef Expression
1 ffnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffn 5384 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5230  wf 5231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f 5239
This theorem is referenced by:  offeq  6121  difinfsn  7130  ctssdc  7143  nnnninfeq  7157  nninfdcinf  7200  nninfwlporlemd  7201  nninfwlporlem  7202  seqvalcd  10492  seq3feq2  10503  seq3feq  10505  seqfeq3  10545  ser0f  10549  facnn  10742  fac0  10743  resunimafz0  10846  seq3shft  10882  fisumss  11435  prodf1f  11586  efcvgfsum  11710  ennnfonelemfun  12471  ennnfonelemf1  12472  mhmf1o  12937  resmhm2b  12956  mhmima  12958  mhmeql  12959  grpinvf1o  13029  ghmrn  13213  ghmpreima  13222  ghmeql  13223  ghmnsgima  13224  ghmnsgpreima  13225  ghmeqker  13227  ghmf1o  13231  rhmf1o  13535  psrbaglesuppg  13967  cnrest2  14213  lmss  14223  lmtopcnp  14227  upxp  14249  uptx  14251  cnmpt11  14260  cnmpt21  14268  cnmpt22f  14272  cnmptcom  14275  hmeof1o2  14285  psmetxrge0  14309  isxmet2d  14325  blelrnps  14396  blelrn  14397  xmetresbl  14417  comet  14476  bdxmet  14478  xmettx  14487  dvidlemap  14637  dvaddxxbr  14642  dvmulxxbr  14643  dvrecap  14654  nninfall  15237  nninfsellemeqinf  15244  nninffeq  15248  refeq  15255
  Copyright terms: Public domain W3C validator