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 5184 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wss 3111 cid 4260 ccnv 4597 ccom 4602 wrel 4603 wfun 5176 |
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-fun 5184 |
This theorem is referenced by: 0nelfun 5200 funeu 5207 nfunv 5215 funopg 5216 funssres 5224 funun 5226 fununi 5250 funcnvres2 5257 funimaexg 5266 fnrel 5280 fcoi1 5362 f1orel 5429 funbrfv 5519 funbrfv2b 5525 fvmptss2 5555 mptrcl 5562 elfvmptrab1 5574 funfvbrb 5592 fmptco 5645 funresdfunsnss 5682 elmpocl 6030 mpoxopn0yelv 6198 tfrlem6 6275 funresdfunsndc 6465 pmresg 6633 fundmen 6763 caseinl 7047 caseinr 7048 axaddf 7800 axmulf 7801 hashinfom 10680 structcnvcnv 12353 istopon 12558 eltg4i 12602 eltg3 12604 tg1 12606 tg2 12607 tgclb 12612 lmrcl 12738 |
Copyright terms: Public domain | W3C validator |