Theorem ffn 5046

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

Syntax hints:   → wi 4   ⊆ wss 2917  ran crn 4346   Fn wfn 4897  ⟶wf 4898

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110  df-f 4906

This theorem is referenced by:  ffun  5048  frel  5049  fdm  5050  fresin  5068  fcoi1  5070  feu  5072  fnconstg  5084  f1fn  5093  fofn  5108  dffo2  5110  f1ofn  5127  feqmptd  5226  fvco3  5244  ffvelrn  5300  dff2  5311  dffo3  5314  dffo4  5315  dffo5  5316  f1ompt  5320  ffnfv  5323  fcompt  5333  fsn2  5337  fconst2g  5376  fconstfvm  5379  fex  5388  dff13  5407  cocan1  5427  off  5724  suppssof1  5728  ofco  5729  caofref  5732  caofrss  5735  caoftrn  5736  fo1stresm  5788  fo2ndresm  5789  1stcof  5790  2ndcof  5791  fo2ndf  5848  tposf2  5883  smoiso  5917  dfz2  8313  uzn0  8488  unirnioo  8842  dfioo2  8843  ioorebasg  8844  fzen  8907  fseq1p1m1  8956  2ffzeq  8998  fvinim0ffz  9096  iser0f  9251  shftf  9431  uzin2  9586  rexanuz  9587