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  9717  uzn0  9938  unirnioo  10375  dfioo2  10376  ioorebasg  10377  fzen  10447  fseq1p1m1  10501  2ffzeq  10548  fvinim0ffz  10660  frecuzrdglem  10848  frecuzrdgtcl  10849  frecuzrdg0  10850  frecuzrdgfunlem  10856  frecuzrdg0t  10859  seq3val  10897  seqvalcd  10898  ser0f  10971  ffz0hash  11276  fnfzo0hash  11278  wrdred1hash  11348  shftf  11595  uzin2  11753  rexanuz  11754  prodf1f  12310  eff2  12447  reeff1  12467  tanvalap  12475  1arithlem4  13145  1arith  13146  isgrpinv  13859  kerf1ghm  14077  cnfldadd  14899  cnfldmul  14901  cnfldplusf  14911  cnfldsub  14912  znunit  14994  psrbaglecl  15060  lmbr2  15315  cncnpi  15329  cncnp  15331  cnpdis  15343  lmff  15350  tx1cn  15370  tx2cn  15371  upxp  15373  txcnmpt  15374  uptx  15375  xmettpos  15471  blrnps  15512  blrn  15513  xmeterval  15536  qtopbasss  15622  cnbl0  15635  cnblcld  15636  cnfldms  15637  tgioo  15655  tgqioo  15656  dvfre  15811  plyreres  15865  reeff1o  15874  pilem1  15880  ioocosf1o  15955  dfrelog  15961  mpodvdsmulf1o  16104  fsumdvdsmul  16105  012of  17023  2o01f  17024  taupi  17123