Theorem ffn 5489

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

Syntax hints:   -> wi 4   C_ wss 3201   ran crn 4732   Fn wfn 5328   -->wf 5329

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

This theorem depends on definitions:  df-bi 117  df-f 5337

This theorem is referenced by:  ffnd  5490  ffun  5492  frel  5494  fdm  5495  fresin  5523  fcoi1  5525  feu  5527  f0bi  5538  fnconstg  5543  f1fn  5553  fofn  5570  dffo2  5572  fimadmfo  5577  f1ofn  5593  fdmeu  5698  feqmptd  5708  fvco3  5726  ffvelcdm  5788  dff2  5799  dffo3  5802  dffo4  5803  dffo5  5804  f1ompt  5806  ffnfv  5813  fcompt  5825  fsn2  5829  fconst2g  5877  fconstfvm  5880  fdmexb  5886  fex  5893  dff13  5919  cocan1  5938  off  6257  suppssof1  6262  ofco  6263  caofref  6269  caofrss  6276  caoftrn  6277  fo1stresm  6333  fo2ndresm  6334  1stcof  6335  2ndcof  6336  fo2ndf  6401  fsuppeq  6425  fsuppeqg  6426  tposf2  6477  smoiso  6511  tfrcllemssrecs  6561  tfrcllemsucaccv  6563  elmapfn  6883  mapsn  6902  pw2f1odclem  7063  mapen  7075  updjudhcoinlf  7339  updjudhcoinrg  7340  updjud  7341  omp1eomlem  7353  dfz2  9613  uzn0  9833  unirnioo  10269  dfioo2  10270  ioorebasg  10271  fzen  10340  fseq1p1m1  10391  2ffzeq  10438  fvinim0ffz  10550  frecuzrdglem  10736  frecuzrdgtcl  10737  frecuzrdg0  10738  frecuzrdgfunlem  10744  frecuzrdg0t  10747  seq3val  10785  seqvalcd  10786  ser0f  10859  ffz0hash  11160  fnfzo0hash  11162  wrdred1hash  11223  shftf  11470  uzin2  11627  rexanuz  11628  prodf1f  12184  eff2  12321  reeff1  12341  tanvalap  12349  1arithlem4  13019  1arith  13020  isgrpinv  13717  kerf1ghm  13941  cnfldadd  14658  cnfldmul  14660  cnfldplusf  14670  cnfldsub  14671  znunit  14755  psrbaglecl  14771  lmbr2  15025  cncnpi  15039  cncnp  15041  cnpdis  15053  lmff  15060  tx1cn  15080  tx2cn  15081  upxp  15083  txcnmpt  15084  uptx  15085  xmettpos  15181  blrnps  15222  blrn  15223  xmeterval  15246  qtopbasss  15332  cnbl0  15345  cnblcld  15346  cnfldms  15347  tgioo  15365  tgqioo  15366  dvfre  15521  plyreres  15575  reeff1o  15584  pilem1  15590  ioocosf1o  15665  dfrelog  15671  mpodvdsmulf1o  15804  fsumdvdsmul  15805  012of  16713  2o01f  16714  taupi  16806