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 5126 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cdm 4539 wfun 5117 wfn 5118 |
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 5126 |
This theorem is referenced by: fnrel 5221 funfni 5223 fnco 5231 fnssresb 5235 ffun 5275 f1fun 5331 f1ofun 5369 fnbrfvb 5462 fvelimab 5477 fvun1 5487 elpreima 5539 respreima 5548 fconst3m 5639 fnfvima 5652 fnunirn 5668 f1eqcocnv 5692 fnexALT 6011 tfrlem4 6210 tfrlem5 6211 fndmeng 6704 caseinl 6976 caseinr 6977 shftfn 10596 phimullem 11901 qnnen 11944 |
Copyright terms: Public domain | W3C validator |