Theorem ffn 5337

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 5192	. 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 3116   ran crn 4605   Fn wfn 5183   -->wf 5184

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 5192

This theorem is referenced by:  ffnd  5338  ffun  5340  frel  5342  fdm  5343  fresin  5366  fcoi1  5368  feu  5370  f0bi  5380  fnconstg  5385  f1fn  5395  fofn  5412  dffo2  5414  f1ofn  5433  feqmptd  5539  fvco3  5557  ffvelrn  5618  dff2  5629  dffo3  5632  dffo4  5633  dffo5  5634  f1ompt  5636  ffnfv  5643  fcompt  5655  fsn2  5659  fconst2g  5700  fconstfvm  5703  fex  5714  dff13  5736  cocan1  5755  off  6062  suppssof1  6067  ofco  6068  caofref  6071  caofrss  6074  caoftrn  6075  fo1stresm  6129  fo2ndresm  6130  1stcof  6131  2ndcof  6132  fo2ndf  6195  tposf2  6236  smoiso  6270  tfrcllemssrecs  6320  tfrcllemsucaccv  6322  elmapfn  6637  mapsn  6656  mapen  6812  updjudhcoinlf  7045  updjudhcoinrg  7046  updjud  7047  omp1eomlem  7059  dfz2  9263  uzn0  9481  unirnioo  9909  dfioo2  9910  ioorebasg  9911  fzen  9978  fseq1p1m1  10029  2ffzeq  10076  fvinim0ffz  10176  frecuzrdglem  10346  frecuzrdgtcl  10347  frecuzrdg0  10348  frecuzrdgfunlem  10354  frecuzrdg0t  10357  seq3val  10393  seqvalcd  10394  ser0f  10450  ffz0hash  10746  fnfzo0hash  10748  shftf  10772  uzin2  10929  rexanuz  10930  prodf1f  11484  eff2  11621  reeff1  11641  tanvalap  11649  1arithlem4  12296  1arith  12297  lmbr2  12854  cncnpi  12868  cncnp  12870  cnpdis  12882  lmff  12889  tx1cn  12909  tx2cn  12910  upxp  12912  txcnmpt  12913  uptx  12914  xmettpos  13010  blrnps  13051  blrn  13052  xmeterval  13075  qtopbasss  13161  cnbl0  13174  cnblcld  13175  tgioo  13186  tgqioo  13187  dvfre  13314  reeff1o  13334  pilem1  13340  ioocosf1o  13415  dfrelog  13421  012of  13875  2o01f  13876  taupi  13949