![]() |
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 6654 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6542 Fn wfn 6543 |
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 206 df-an 396 df-fn 6551 |
This theorem is referenced by: imadrhmcl 20685 noseqrdg0 28193 noseqrdgsuc 28194 ply1degltdimlem 33320 bnj945 34404 bnj545 34526 bnj548 34528 bnj553 34529 bnj570 34536 bnj929 34567 bnj966 34575 bnj1442 34680 bnj1450 34681 bnj1501 34698 aks6d1c2lem4 41598 aks6d1c2 41601 aks6d1c6lem5 41649 eqresfnbd 41723 |
Copyright terms: Public domain | W3C validator |