Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fnfun | Unicode version |
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fnfun |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 5199 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 cdm 4609 wfun 5190 wfn 5191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-fn 5199 |
This theorem is referenced by: fnrel 5294 funfni 5296 fnco 5304 fnssresb 5308 ffun 5348 f1fun 5404 f1ofun 5442 fnbrfvb 5535 fvelimab 5550 fvun1 5560 elpreima 5613 respreima 5622 fconst3m 5713 fnfvima 5728 fnunirn 5744 f1eqcocnv 5768 fnexALT 6088 tfrlem4 6290 tfrlem5 6291 fndmeng 6786 caseinl 7066 caseinr 7067 cc2lem 7221 shftfn 10781 phimullem 12172 qnnen 12379 |
Copyright terms: Public domain | W3C validator |