Theorem ffn 5510

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

Assertion

Ref	Expression
ffn	⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 5358	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3213  ran crn 4752   Fn wfn 5349  ⟶wf 5350

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 5358

This theorem is referenced by:  ffnd  5511  ffun  5513  frel  5515  fdm  5516  ffrn  5522  fresin  5545  fresaunres2disj  5547  fcoi1  5549  feu  5551  f0bi  5562  fnconstg  5567  f1fn  5577  fofn  5594  dffo2  5596  fimadmfo  5601  f1ofn  5617  fdmeu  5722  feqmptd  5732  fvco3  5750  ffvelcdm  5812  dff2  5823  dffo3  5826  dffo4  5827  dffo5  5828  f1ompt  5830  ffnfv  5837  fcompt  5849  fsn2  5853  fconst2g  5901  fconstfvm  5904  fdmexb  5910  fex  5917  dff13  5943  cocan1  5962  off  6281  suppssof1  6286  ofco  6287  caofref  6293  caofrss  6300  caoftrn  6301  fo1stresm  6357  fo2ndresm  6358  1stcof  6359  2ndcof  6360  fo2ndf  6425  fsuppeq  6449  fsuppeqg  6450  tposf2  6501  smoiso  6535  tfrcllemssrecs  6585  tfrcllemsucaccv  6587  elmapfn  6907  mapsnd  6925  mapsn  6927  pw2f1odclem  7089  mapen  7101  mapunen  7106  updjudhcoinlf  7373  updjudhcoinrg  7374  updjud  7375  omp1eomlem  7387  dfz2  9652  uzn0  9873  unirnioo  10309  dfioo2  10310  ioorebasg  10311  fzen  10380  fseq1p1m1  10432  2ffzeq  10479  fvinim0ffz  10591  frecuzrdglem  10777  frecuzrdgtcl  10778  frecuzrdg0  10779  frecuzrdgfunlem  10785  frecuzrdg0t  10788  seq3val  10826  seqvalcd  10827  ser0f  10900  ffz0hash  11204  fnfzo0hash  11206  wrdred1hash  11272  shftf  11519  uzin2  11676  rexanuz  11677  prodf1f  12233  eff2  12370  reeff1  12390  tanvalap  12398  1arithlem4  13068  1arith  13069  isgrpinv  13784  kerf1ghm  14008  cnfldadd  14727  cnfldmul  14729  cnfldplusf  14739  cnfldsub  14740  znunit  14824  psrbaglecl  14841  lmbr2  15096  cncnpi  15110  cncnp  15112  cnpdis  15124  lmff  15131  tx1cn  15151  tx2cn  15152  upxp  15154  txcnmpt  15155  uptx  15156  xmettpos  15252  blrnps  15293  blrn  15294  xmeterval  15317  qtopbasss  15403  cnbl0  15416  cnblcld  15417  cnfldms  15418  tgioo  15436  tgqioo  15437  dvfre  15592  plyreres  15646  reeff1o  15655  pilem1  15661  ioocosf1o  15736  dfrelog  15742  mpodvdsmulf1o  15875  fsumdvdsmul  15876  012of  16784  2o01f  16785  taupi  16876