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

Theorem ffnd 5273
 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 5272 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝜑𝐹 Fn 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   Fn wfn 5118  ⟶wf 5119 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 5127 This theorem is referenced by:  offeq  5995  difinfsn  6985  ctssdc  6998  seqvalcd  10239  seq3feq2  10250  seq3feq  10252  seqfeq3  10292  ser0f  10295  facnn  10480  fac0  10481  resunimafz0  10581  seq3shft  10617  fisumss  11168  prodf1f  11319  efcvgfsum  11380  ennnfonelemfun  11937  ennnfonelemf1  11938  cnrest2  12415  lmss  12425  lmtopcnp  12429  upxp  12451  uptx  12453  cnmpt11  12462  cnmpt21  12470  cnmpt22f  12474  cnmptcom  12477  hmeof1o2  12487  psmetxrge0  12511  isxmet2d  12527  blelrnps  12598  blelrn  12599  xmetresbl  12619  comet  12678  bdxmet  12680  xmettx  12689  dvidlemap  12839  dvaddxxbr  12844  dvmulxxbr  12845  dvrecap  12856  nninfalllemn  13232  nninfall  13234  nninfsellemeqinf  13242  nninffeq  13246  refeq  13253
 Copyright terms: Public domain W3C validator