![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fnrel | Unicode version |
Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fnrel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 5332 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | funrel 5252 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 df-fn 5238 |
This theorem is referenced by: fnbr 5337 fnresdm 5344 fn0 5354 frel 5389 fcoi2 5416 f1rel 5444 f1ocnv 5493 dffn5im 5581 fnex 5758 fnexALT 6135 basmex 12570 basmexd 12571 ismgmn0 12831 istps 13984 topontopn 13989 cldrcl 14054 neiss2 14094 |
Copyright terms: Public domain | W3C validator |