Theorem ffn 5533

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ran crn 4775   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5381

This theorem is used by:  ffnd  5534  ffun  5536  frel  5538  fdm  5539  ffrn  5545  fresin  5568  fresaunres2disj  5570  fcoi1  5572  feu  5574  f0bi  5585  fnconstg  5590  f1fn  5600  fofn  5617  dffo2  5619  fimadmfo  5624  f1ofn  5640  fdmeu  5746  feqmptd  5756  fvco3  5776  ffvelcdm  5841  dff2  5852  dffo3  5855  dffo4  5856  dffo5  5857  f1ompt  5859  ffnfv  5866  fcompt  5878  fsn2  5882  fconst2g  5930  fconstfvm  5933  fdmexb  5939  fex  5947  dff13  5974  cocan1  5993  off  6315  suppssof1  6320  ofco  6321  caofref  6327  caofrss  6334  caoftrn  6335  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  fo2ndf  6463  fsuppeq  6487  fsuppeqg  6488  tposf2  6539  smoiso  6573  tfrcllemssrecs  6623  tfrcllemsucaccv  6625  elmapfn  6952  mapsnd  6970  mapsn  6972  pw2f1odclem  7134  mapen  7146  mapunen  7151  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  omp1eomlem  7434  dfz2  9721  uzn0  9947  unirnioo  10385  dfioo2  10386  ioorebasg  10387  fzen  10457  fseq1p1m1  10511  2ffzeq  10558  fvinim0ffz  10670  frecuzrdglem  10861  frecuzrdgtcl  10862  frecuzrdg0  10863  frecuzrdgfunlem  10869  frecuzrdg0t  10872  seq3val  10910  seqvalcd  10911  ser0f  10984  ffz0hash  11290  fnfzo0hash  11292  wrdred1hash  11362  shftf  11609  uzin2  11767  rexanuz  11768  prodf1f  12326  eff2  12463  reeff1  12483  tanvalap  12491  1arithlem4  13165  1arith  13166  isgrpinv  13908  kerf1ghm  14126  cnfldadd  14948  cnfldmul  14950  cnfldplusf  14960  cnfldsub  14961  znunit  15043  psrbaglecl  15109  lmbr2  15364  cncnpi  15378  cncnp  15380  cnpdis  15392  lmff  15399  tx1cn  15419  tx2cn  15420  upxp  15422  txcnmpt  15423  uptx  15424  xmettpos  15520  blrnps  15561  blrn  15562  xmeterval  15585  qtopbasss  15671  cnbl0  15684  cnblcld  15685  cnfldms  15686  tgioo  15704  tgqioo  15705  dvfre  15860  plyreres  15914  reeff1o  15923  pilem1  15930  ioocosf1o  16005  dfrelog  16011  mpodvdsmulf1o  16185  fsumdvdsmul  16186  012of  17121  2o01f  17122  taupi  17221