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

Theorem fnfun 5188
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5094 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 270 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  dom cdm 4507  Fun wfun 5085   Fn wfn 5086
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-fn 5094
This theorem is referenced by:  fnrel  5189  funfni  5191  fnco  5199  fnssresb  5203  ffun  5243  f1fun  5299  f1ofun  5335  fnbrfvb  5428  fvelimab  5443  fvun1  5453  elpreima  5505  respreima  5514  fconst3m  5605  fnfvima  5618  fnunirn  5634  f1eqcocnv  5658  fnexALT  5977  tfrlem4  6176  tfrlem5  6177  fndmeng  6670  caseinl  6942  caseinr  6943  shftfn  10536  phimullem  11796  qnnen  11839
  Copyright terms: Public domain W3C validator