Theorem ffn 5174

Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
ffn	|- ( F : A --> B -> F Fn A )

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 5032	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simplbi 269	1 |- ( F : A --> B -> F Fn A )

Syntax hints:   -> wi 4   C_ wss 3000   ran crn 4453   Fn wfn 5023   -->wf 5024

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f 5032

This theorem is referenced by:  ffnd  5175  ffun  5177  frel  5178  fdm  5179  fresin  5202  fcoi1  5204  feu  5206  f0bi  5216  fnconstg  5221  f1fn  5231  fofn  5248  dffo2  5250  f1ofn  5267  feqmptd  5370  fvco3  5388  ffvelrn  5446  dff2  5457  dffo3  5460  dffo4  5461  dffo5  5462  f1ompt  5464  ffnfv  5470  fcompt  5481  fsn2  5485  fconst2g  5526  fconstfvm  5529  fex  5538  dff13  5561  cocan1  5580  off  5882  suppssof1  5886  ofco  5887  caofref  5890  caofrss  5893  caoftrn  5894  fo1stresm  5946  fo2ndresm  5947  1stcof  5948  2ndcof  5949  fo2ndf  6006  tposf2  6047  smoiso  6081  tfrcllemssrecs  6131  tfrcllemsucaccv  6133  elmapfn  6442  mapsn  6461  mapen  6616  updjudhcoinlf  6825  updjudhcoinrg  6826  updjud  6827  dfz2  8880  uzn0  9095  unirnioo  9452  dfioo2  9453  ioorebasg  9454  fzen  9518  fseq1p1m1  9569  2ffzeq  9613  fvinim0ffz  9713  frecuzrdglem  9879  frecuzrdgtcl  9880  frecuzrdg0  9881  frecuzrdgfunlem  9887  frecuzrdg0t  9890  iseqvalt  9934  seq3val  9935  iseqoveq  9946  iseqsst  9947  iseqfeq2  9952  iseqfeq  9957  iser0f  10009  ser0f  10011  facnn  10196  fac0  10197  ffz0hash  10299  fnfzo0hash  10301  shftf  10325  uzin2  10481  rexanuz  10482  eff2  11031  reeff1  11052  tanvalap  11060