Theorem ffn 5513

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

Syntax hints:   → wi 4   ⊆ wss 3214  ran crn 4755   Fn wfn 5352  ⟶wf 5353

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 5361

This theorem is referenced by:  ffnd  5514  ffun  5516  frel  5518  fdm  5519  ffrn  5525  fresin  5548  fresaunres2disj  5550  fcoi1  5552  feu  5554  f0bi  5565  fnconstg  5570  f1fn  5580  fofn  5597  dffo2  5599  fimadmfo  5604  f1ofn  5620  fdmeu  5725  feqmptd  5735  fvco3  5753  ffvelcdm  5815  dff2  5826  dffo3  5829  dffo4  5830  dffo5  5831  f1ompt  5833  ffnfv  5840  fcompt  5852  fsn2  5856  fconst2g  5904  fconstfvm  5907  fdmexb  5913  fex  5920  dff13  5947  cocan1  5966  off  6288  suppssof1  6293  ofco  6294  caofref  6300  caofrss  6307  caoftrn  6308  fo1stresm  6368  fo2ndresm  6369  1stcof  6370  2ndcof  6371  fo2ndf  6436  fsuppeq  6460  fsuppeqg  6461  tposf2  6512  smoiso  6546  tfrcllemssrecs  6596  tfrcllemsucaccv  6598  elmapfn  6918  mapsnd  6936  mapsn  6938  pw2f1odclem  7100  mapen  7112  mapunen  7117  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  omp1eomlem  7398  dfz2  9667  uzn0  9888  unirnioo  10325  dfioo2  10326  ioorebasg  10327  fzen  10397  fseq1p1m1  10450  2ffzeq  10497  fvinim0ffz  10609  frecuzrdglem  10797  frecuzrdgtcl  10798  frecuzrdg0  10799  frecuzrdgfunlem  10805  frecuzrdg0t  10808  seq3val  10846  seqvalcd  10847  ser0f  10920  ffz0hash  11225  fnfzo0hash  11227  wrdred1hash  11293  shftf  11540  uzin2  11697  rexanuz  11698  prodf1f  12254  eff2  12391  reeff1  12411  tanvalap  12419  1arithlem4  13089  1arith  13090  isgrpinv  13809  kerf1ghm  14027  cnfldadd  14836  cnfldmul  14838  cnfldplusf  14848  cnfldsub  14849  znunit  14933  psrbaglecl  14950  lmbr2  15205  cncnpi  15219  cncnp  15221  cnpdis  15233  lmff  15240  tx1cn  15260  tx2cn  15261  upxp  15263  txcnmpt  15264  uptx  15265  xmettpos  15361  blrnps  15402  blrn  15403  xmeterval  15426  qtopbasss  15512  cnbl0  15525  cnblcld  15526  cnfldms  15527  tgioo  15545  tgqioo  15546  dvfre  15701  plyreres  15755  reeff1o  15764  pilem1  15770  ioocosf1o  15845  dfrelog  15851  mpodvdsmulf1o  15984  fsumdvdsmul  15985  012of  16893  2o01f  16894  taupi  16985