![]() |
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 6679 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6567 Fn wfn 6568 |
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 6576 |
This theorem is referenced by: imadrhmcl 20820 noseqrdg0 28331 noseqrdgsuc 28332 ply1degltdimlem 33635 bnj945 34749 bnj545 34871 bnj548 34873 bnj553 34874 bnj570 34881 bnj929 34912 bnj966 34920 bnj1442 35025 bnj1450 35026 bnj1501 35043 aks6d1c2lem4 42084 aks6d1c2 42087 aks6d1c6lem5 42134 eqresfnbd 42227 |
Copyright terms: Public domain | W3C validator |