![]() |
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 5018 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 268 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 df-fn 5018 |
This theorem is referenced by: fnrel 5112 funfni 5114 fnco 5122 fnssresb 5126 ffun 5164 f1fun 5219 f1ofun 5255 fnbrfvb 5345 fvelimab 5360 fvun1 5370 elpreima 5418 respreima 5427 fconst3m 5516 fnfvima 5529 fnunirn 5546 f1eqcocnv 5570 fnexALT 5884 tfrlem4 6078 tfrlem5 6079 fndmeng 6525 shftfn 10254 phimullem 11475 |
Copyright terms: Public domain | W3C validator |