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

Theorem ffn 5074
Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
ffn (𝐹:𝐴𝐵𝐹 Fn 𝐴)

Proof of Theorem ffn
StepHypRef Expression
1 df-f 4934 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simplbi 263 1 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2945  ran crn 4374   Fn wfn 4925  wf 4926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-f 4934
This theorem is referenced by:  ffun  5076  frel  5077  fdm  5078  fresin  5096  fcoi1  5098  feu  5100  fnconstg  5112  f1fn  5121  fofn  5136  dffo2  5138  f1ofn  5155  feqmptd  5254  fvco3  5272  ffvelrn  5328  dff2  5339  dffo3  5342  dffo4  5343  dffo5  5344  f1ompt  5348  ffnfv  5351  fcompt  5361  fsn2  5365  fconst2g  5404  fconstfvm  5407  fex  5416  dff13  5435  cocan1  5455  off  5752  suppssof1  5756  ofco  5757  caofref  5760  caofrss  5763  caoftrn  5764  fo1stresm  5816  fo2ndresm  5817  1stcof  5818  2ndcof  5819  fo2ndf  5876  tposf2  5914  smoiso  5948  dfz2  8371  uzn0  8584  unirnioo  8943  dfioo2  8944  ioorebasg  8945  fzen  9009  fseq1p1m1  9058  2ffzeq  9100  fvinim0ffz  9198  iser0f  9416  shftf  9659  uzin2  9814  rexanuz  9815
  Copyright terms: Public domain W3C validator