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  6589  tfrlem5  6590  fndmeng  7104  fczfsuppd  7305  caseinl  7438  caseinr  7439  cc2lem  7639  shftfn  11611  phimullem  13032  qnnen  13380  imasaddvallemg  13695  prdsex  14279  prdsval  14280  prdsbaslemss  14281  lidlmex  14921  edgstruct  16543  upgredg  16623