|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > fnfund | Structured version Visualization version GIF version | ||
| Description: A function with domain is a function, deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) | 
| Ref | Expression | 
|---|---|
| fnfund.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| Ref | Expression | 
|---|---|
| fnfund | ⊢ (𝜑 → Fun 𝐹) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | fnfund.1 | . 2 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
| 2 | fnfun 6667 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Fun 𝐹) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 Fun wfun 6554 Fn wfn 6555 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-fn 6563 | 
| This theorem is referenced by: imadrhmcl 20799 noseqrdg0 28314 noseqrdgsuc 28315 ply1degltdimlem 33674 bnj945 34788 bnj545 34910 bnj548 34912 bnj553 34913 bnj570 34920 bnj929 34951 bnj966 34959 bnj1442 35064 bnj1450 35065 bnj1501 35082 aks6d1c2lem4 42129 aks6d1c2 42132 aks6d1c6lem5 42179 eqresfnbd 42273 | 
| Copyright terms: Public domain | W3C validator |