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

Theorem fnfun 5260
 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 5166 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 272 1 (𝐹 Fn 𝐴 → Fun 𝐹)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332  dom cdm 4579  Fun wfun 5157   Fn wfn 5158 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 5166 This theorem is referenced by:  fnrel  5261  funfni  5263  fnco  5271  fnssresb  5275  ffun  5315  f1fun  5371  f1ofun  5409  fnbrfvb  5502  fvelimab  5517  fvun1  5527  elpreima  5579  respreima  5588  fconst3m  5679  fnfvima  5692  fnunirn  5708  f1eqcocnv  5732  fnexALT  6051  tfrlem4  6250  tfrlem5  6251  fndmeng  6744  caseinl  7021  caseinr  7022  cc2lem  7165  shftfn  10701  phimullem  12068  qnnen  12111
 Copyright terms: Public domain W3C validator