Theorem ffn 5482

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

Syntax hints:   → wi 4   ⊆ wss 3200  ran crn 4726   Fn wfn 5321  ⟶wf 5322

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 5330

This theorem is referenced by:  ffnd  5483  ffun  5485  frel  5487  fdm  5488  fresin  5515  fcoi1  5517  feu  5519  f0bi  5529  fnconstg  5534  f1fn  5544  fofn  5561  dffo2  5563  fimadmfo  5568  f1ofn  5584  fdmeu  5689  feqmptd  5699  fvco3  5717  ffvelcdm  5780  dff2  5791  dffo3  5794  dffo4  5795  dffo5  5796  f1ompt  5798  ffnfv  5805  fcompt  5817  fsn2  5821  fconst2g  5869  fconstfvm  5872  fex  5883  dff13  5909  cocan1  5928  off  6248  suppssof1  6253  ofco  6254  caofref  6260  caofrss  6267  caoftrn  6268  fo1stresm  6324  fo2ndresm  6325  1stcof  6326  2ndcof  6327  fo2ndf  6392  tposf2  6434  smoiso  6468  tfrcllemssrecs  6518  tfrcllemsucaccv  6520  elmapfn  6840  mapsn  6859  pw2f1odclem  7020  mapen  7032  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eomlem  7293  dfz2  9552  uzn0  9772  unirnioo  10208  dfioo2  10209  ioorebasg  10210  fzen  10278  fseq1p1m1  10329  2ffzeq  10376  fvinim0ffz  10488  frecuzrdglem  10674  frecuzrdgtcl  10675  frecuzrdg0  10676  frecuzrdgfunlem  10682  frecuzrdg0t  10685  seq3val  10723  seqvalcd  10724  ser0f  10797  ffz0hash  11098  fnfzo0hash  11100  wrdred1hash  11161  shftf  11395  uzin2  11552  rexanuz  11553  prodf1f  12109  eff2  12246  reeff1  12266  tanvalap  12274  1arithlem4  12944  1arith  12945  isgrpinv  13642  kerf1ghm  13866  cnfldadd  14582  cnfldmul  14584  cnfldplusf  14594  cnfldsub  14595  znunit  14679  lmbr2  14944  cncnpi  14958  cncnp  14960  cnpdis  14972  lmff  14979  tx1cn  14999  tx2cn  15000  upxp  15002  txcnmpt  15003  uptx  15004  xmettpos  15100  blrnps  15141  blrn  15142  xmeterval  15165  qtopbasss  15251  cnbl0  15264  cnblcld  15265  cnfldms  15266  tgioo  15284  tgqioo  15285  dvfre  15440  plyreres  15494  reeff1o  15503  pilem1  15509  ioocosf1o  15584  dfrelog  15590  mpodvdsmulf1o  15720  fsumdvdsmul  15721  012of  16618  2o01f  16619  taupi  16704