Theorem ffn 5066

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 4926	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2	1	simplbi 268	1 |- ( F : A --> B -> F Fn A )

Syntax hints:   -> wi 4   C_ wss 2973   ran crn 4364   Fn wfn 4917   -->wf 4918

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

This theorem depends on definitions:  df-bi 115  df-f 4926

This theorem is referenced by:  ffun  5068  frel  5069  fdm  5070  fresin  5088  fcoi1  5090  feu  5092  fnconstg  5104  f1fn  5113  fofn  5128  dffo2  5130  f1ofn  5147  feqmptd  5247  fvco3  5265  ffvelrn  5321  dff2  5332  dffo3  5335  dffo4  5336  dffo5  5337  f1ompt  5341  ffnfv  5344  fcompt  5354  fsn2  5358  fconst2g  5397  fconstfvm  5400  fex  5409  dff13  5428  cocan1  5447  off  5744  suppssof1  5748  ofco  5749  caofref  5752  caofrss  5755  caoftrn  5756  fo1stresm  5808  fo2ndresm  5809  1stcof  5810  2ndcof  5811  fo2ndf  5868  tposf2  5906  smoiso  5940  dfz2  8420  uzn0  8634  unirnioo  8996  dfioo2  8997  ioorebasg  8998  fzen  9062  fseq1p1m1  9111  2ffzeq  9151  fvinim0ffz  9250  iser0f  9472  shftf  9718  uzin2  9873  rexanuz  9874  eucialg  10441