Theorem ffn 4989

Description: A mapping is a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
ffn	⊢ (𝐹:A⟶B → 𝐹 Fn A)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 4849	. 2 ⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B))
2	1	simplbi 259	1 ⊢ (𝐹:A⟶B → 𝐹 Fn A)

Syntax hints:   → wi 4   ⊆ wss 2911  ran crn 4289   Fn wfn 4840  ⟶wf 4841

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 4849

This theorem is referenced by:  ffun  4991  frel  4992  fdm  4993  fresin  5011  fcoi1  5013  feu  5015  fnconstg  5027  f1fn  5036  fofn  5051  dffo2  5053  f1ofn  5070  feqmptd  5169  fvco3  5187  ffvelrn  5243  dff2  5254  dffo3  5257  dffo4  5258  dffo5  5259  f1ompt  5263  ffnfv  5266  fcompt  5276  fsn2  5280  fconst2g  5319  fconstfvm  5322  fex  5331  dff13  5350  cocan1  5370  off  5666  suppssof1  5670  ofco  5671  caofref  5674  caofrss  5677  caoftrn  5678  fo1stresm  5730  fo2ndresm  5731  1stcof  5732  2ndcof  5733  fo2ndf  5790  tposf2  5824  smoiso  5858  dfz2  8049  uzn0  8224  unirnioo  8572  dfioo2  8573  ioorebasg  8574  fzen  8637  fseq1p1m1  8686  2ffzeq  8728