Theorem ffn 5280

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

Syntax hints:   -> wi 4   C_ wss 3076   ran crn 4548   Fn wfn 5126   -->wf 5127

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-f 5135

This theorem is referenced by:  ffnd  5281  ffun  5283  frel  5285  fdm  5286  fresin  5309  fcoi1  5311  feu  5313  f0bi  5323  fnconstg  5328  f1fn  5338  fofn  5355  dffo2  5357  f1ofn  5376  feqmptd  5482  fvco3  5500  ffvelrn  5561  dff2  5572  dffo3  5575  dffo4  5576  dffo5  5577  f1ompt  5579  ffnfv  5586  fcompt  5598  fsn2  5602  fconst2g  5643  fconstfvm  5646  fex  5655  dff13  5677  cocan1  5696  off  6002  suppssof1  6007  ofco  6008  caofref  6011  caofrss  6014  caoftrn  6015  fo1stresm  6067  fo2ndresm  6068  1stcof  6069  2ndcof  6070  fo2ndf  6132  tposf2  6173  smoiso  6207  tfrcllemssrecs  6257  tfrcllemsucaccv  6259  elmapfn  6573  mapsn  6592  mapen  6748  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  omp1eomlem  6987  dfz2  9147  uzn0  9365  unirnioo  9786  dfioo2  9787  ioorebasg  9788  fzen  9854  fseq1p1m1  9905  2ffzeq  9949  fvinim0ffz  10049  frecuzrdglem  10215  frecuzrdgtcl  10216  frecuzrdg0  10217  frecuzrdgfunlem  10223  frecuzrdg0t  10226  seq3val  10262  seqvalcd  10263  ser0f  10319  ffz0hash  10608  fnfzo0hash  10610  shftf  10634  uzin2  10791  rexanuz  10792  prodf1f  11344  eff2  11423  reeff1  11443  tanvalap  11451  lmbr2  12422  cncnpi  12436  cncnp  12438  cnpdis  12450  lmff  12457  tx1cn  12477  tx2cn  12478  upxp  12480  txcnmpt  12481  uptx  12482  xmettpos  12578  blrnps  12619  blrn  12620  xmeterval  12643  qtopbasss  12729  cnbl0  12742  cnblcld  12743  tgioo  12754  tgqioo  12755  dvfre  12882  reeff1o  12902  pilem1  12908  ioocosf1o  12983  dfrelog  12989  012of  13363  2o01f  13364  taupi  13430