![]() |
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 5237 |
. 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-fun 5237 |
This theorem is referenced by: 0nelfun 5253 funeu 5260 nfunv 5268 funopg 5269 funssres 5277 funun 5279 fununi 5303 funcnvres2 5310 funimaexg 5319 fnrel 5333 fcoi1 5415 f1orel 5483 funbrfv 5574 funbrfv2b 5580 fvmptss2 5611 mptrcl 5618 elfvmptrab1 5630 funfvbrb 5649 fmptco 5702 funresdfunsnss 5739 elmpocl 6090 funexw 6136 mpoxopn0yelv 6263 tfrlem6 6340 funresdfunsndc 6530 pmresg 6701 fundmen 6831 caseinl 7119 caseinr 7120 axaddf 7896 axmulf 7897 hashinfom 10789 4sqlemffi 12427 structcnvcnv 12527 lidlmex 13788 istopon 13965 eltg4i 14007 eltg3 14009 tg1 14011 tg2 14012 tgclb 14017 lmrcl 14143 |
Copyright terms: Public domain | W3C validator |