Theorem ffn 5489

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

Syntax hints:   → wi 4   ⊆ 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  7322  updjudhcoinrg  7323  updjud  7324  omp1eomlem  7336  dfz2  9596  uzn0  9816  unirnioo  10252  dfioo2  10253  ioorebasg  10254  fzen  10323  fseq1p1m1  10374  2ffzeq  10421  fvinim0ffz  10533  frecuzrdglem  10719  frecuzrdgtcl  10720  frecuzrdg0  10721  frecuzrdgfunlem  10727  frecuzrdg0t  10730  seq3val  10768  seqvalcd  10769  ser0f  10842  ffz0hash  11143  fnfzo0hash  11145  wrdred1hash  11206  shftf  11453  uzin2  11610  rexanuz  11611  prodf1f  12167  eff2  12304  reeff1  12324  tanvalap  12332  1arithlem4  13002  1arith  13003  isgrpinv  13700  kerf1ghm  13924  cnfldadd  14641  cnfldmul  14643  cnfldplusf  14653  cnfldsub  14654  znunit  14738  psrbaglecl  14754  lmbr2  15008  cncnpi  15022  cncnp  15024  cnpdis  15036  lmff  15043  tx1cn  15063  tx2cn  15064  upxp  15066  txcnmpt  15067  uptx  15068  xmettpos  15164  blrnps  15205  blrn  15206  xmeterval  15229  qtopbasss  15315  cnbl0  15328  cnblcld  15329  cnfldms  15330  tgioo  15348  tgqioo  15349  dvfre  15504  plyreres  15558  reeff1o  15567  pilem1  15573  ioocosf1o  15648  dfrelog  15654  mpodvdsmulf1o  15787  fsumdvdsmul  15788  012of  16696  2o01f  16697  taupi  16789