Theorem ffn 5472

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 5321	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3197  ran crn 4719   Fn wfn 5312  ⟶wf 5313

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 5321

This theorem is referenced by:  ffnd  5473  ffun  5475  frel  5477  fdm  5478  fresin  5503  fcoi1  5505  feu  5507  f0bi  5517  fnconstg  5522  f1fn  5532  fofn  5549  dffo2  5551  fimadmfo  5556  f1ofn  5572  fdmeu  5676  feqmptd  5686  fvco3  5704  ffvelcdm  5767  dff2  5778  dffo3  5781  dffo4  5782  dffo5  5783  f1ompt  5785  ffnfv  5792  fcompt  5804  fsn2  5808  fconst2g  5853  fconstfvm  5856  fex  5867  dff13  5891  cocan1  5910  off  6229  suppssof1  6234  ofco  6235  caofref  6241  caofrss  6248  caoftrn  6249  fo1stresm  6305  fo2ndresm  6306  1stcof  6307  2ndcof  6308  fo2ndf  6371  tposf2  6412  smoiso  6446  tfrcllemssrecs  6496  tfrcllemsucaccv  6498  elmapfn  6816  mapsn  6835  pw2f1odclem  6991  mapen  7003  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  omp1eomlem  7257  dfz2  9515  uzn0  9734  unirnioo  10165  dfioo2  10166  ioorebasg  10167  fzen  10235  fseq1p1m1  10286  2ffzeq  10333  fvinim0ffz  10442  frecuzrdglem  10628  frecuzrdgtcl  10629  frecuzrdg0  10630  frecuzrdgfunlem  10636  frecuzrdg0t  10639  seq3val  10677  seqvalcd  10678  ser0f  10751  ffz0hash  11050  fnfzo0hash  11052  wrdred1hash  11110  shftf  11336  uzin2  11493  rexanuz  11494  prodf1f  12049  eff2  12186  reeff1  12206  tanvalap  12214  1arithlem4  12884  1arith  12885  isgrpinv  13582  kerf1ghm  13806  cnfldadd  14520  cnfldmul  14522  cnfldplusf  14532  cnfldsub  14533  znunit  14617  lmbr2  14882  cncnpi  14896  cncnp  14898  cnpdis  14910  lmff  14917  tx1cn  14937  tx2cn  14938  upxp  14940  txcnmpt  14941  uptx  14942  xmettpos  15038  blrnps  15079  blrn  15080  xmeterval  15103  qtopbasss  15189  cnbl0  15202  cnblcld  15203  cnfldms  15204  tgioo  15222  tgqioo  15223  dvfre  15378  plyreres  15432  reeff1o  15441  pilem1  15447  ioocosf1o  15522  dfrelog  15528  mpodvdsmulf1o  15658  fsumdvdsmul  15659  012of  16316  2o01f  16317  taupi  16400