![]() |
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 5241 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-fn 5241 |
This theorem is referenced by: fnrel 5336 funfni 5338 fnco 5346 fnssresb 5350 ffun 5390 f1fun 5446 f1ofun 5485 fnbrfvb 5580 fvelimab 5596 fvun1 5606 elpreima 5659 respreima 5668 fconst3m 5759 fnfvima 5775 fnunirn 5792 f1eqcocnv 5816 fnexALT 6140 tfrlem4 6342 tfrlem5 6343 fndmeng 6840 caseinl 7124 caseinr 7125 cc2lem 7300 shftfn 10874 phimullem 12268 qnnen 12493 prdsex 12785 imasaddvallemg 12803 lidlmex 13816 |
Copyright terms: Public domain | W3C validator |