Theorem fnfun 5481

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 5383	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 274	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4776  Fun wfun 5374   Fn wfn 5375

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-fn 5383

This theorem is used by:  fnrel  5482  funfni  5486  fnco  5494  fnssresb  5498  ffun  5539  f1fun  5604  f1ofun  5644  fnbrfvb  5744  fvelimab  5762  fvun1  5772  elpreima  5831  respreima  5839  fncofn  5896  fconst3m  5937  fnfvima  5956  fnunirn  5976  f1eqcocnv  6000  fnexALT  6344  suppvalfng  6484  suppvalfn  6485  suppfnss  6501  tfrlem4  6588  tfrlem5  6589  fndmeng  7103  fczfsuppd  7303  caseinl  7438  caseinr  7439  cc2lem  7639  shftfn  11612  phimullem  13033  qnnen  13381  imasaddvallemg  13696  prdsex  14280  prdsval  14281  prdsbaslemss  14282  lidlmex  14922  edgstruct  16522  upgredg  16602