![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > funrel | Unicode version |
Description: A function is a relation. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
funrel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fun 5083 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 270 |
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 105 |
This theorem depends on definitions: df-bi 116 df-fun 5083 |
This theorem is referenced by: 0nelfun 5099 funeu 5106 nfunv 5114 funopg 5115 funssres 5123 funun 5125 fununi 5149 funcnvres2 5156 funimaexg 5165 fnrel 5179 fcoi1 5261 f1orel 5326 funbrfv 5414 funbrfv2b 5420 fvmptss2 5450 mptrcl 5457 elfvmptrab1 5469 funfvbrb 5487 fmptco 5540 funresdfunsnss 5577 elmpocl 5922 mpoxopn0yelv 6090 tfrlem6 6167 funresdfunsndc 6356 pmresg 6524 fundmen 6654 caseinl 6928 caseinr 6929 axaddf 7603 axmulf 7604 hashinfom 10417 structcnvcnv 11818 istopon 12023 eltg4i 12067 eltg3 12069 tg1 12071 tg2 12072 tgclb 12077 lmrcl 12203 |
Copyright terms: Public domain | W3C validator |