![]() |
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 6669 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6557 Fn wfn 6558 |
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 6566 |
This theorem is referenced by: imadrhmcl 20815 noseqrdg0 28328 noseqrdgsuc 28329 ply1degltdimlem 33650 bnj945 34766 bnj545 34888 bnj548 34890 bnj553 34891 bnj570 34898 bnj929 34929 bnj966 34937 bnj1442 35042 bnj1450 35043 bnj1501 35060 aks6d1c2lem4 42109 aks6d1c2 42112 aks6d1c6lem5 42159 eqresfnbd 42252 |
Copyright terms: Public domain | W3C validator |