![]() |
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 5214 |
. 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 5214 |
This theorem is referenced by: 0nelfun 5230 funeu 5237 nfunv 5245 funopg 5246 funssres 5254 funun 5256 fununi 5280 funcnvres2 5287 funimaexg 5296 fnrel 5310 fcoi1 5392 f1orel 5460 funbrfv 5550 funbrfv2b 5556 fvmptss2 5587 mptrcl 5594 elfvmptrab1 5606 funfvbrb 5625 fmptco 5678 funresdfunsnss 5715 elmpocl 6063 funexw 6107 mpoxopn0yelv 6234 tfrlem6 6311 funresdfunsndc 6501 pmresg 6670 fundmen 6800 caseinl 7084 caseinr 7085 axaddf 7855 axmulf 7856 hashinfom 10739 structcnvcnv 12458 istopon 13171 eltg4i 13215 eltg3 13217 tg1 13219 tg2 13220 tgclb 13225 lmrcl 13351 |
Copyright terms: Public domain | W3C validator |