Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fnrel | GIF version |
Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fnrel | ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 5295 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | funrel 5215 | . 2 ⊢ (Fun 𝐹 → Rel 𝐹) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Rel wrel 4616 Fun wfun 5192 Fn wfn 5193 |
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 5200 df-fn 5201 |
This theorem is referenced by: fnbr 5300 fnresdm 5307 fn0 5317 frel 5352 fcoi2 5379 f1rel 5407 f1ocnv 5455 dffn5im 5542 fnex 5718 fnexALT 6090 basmex 12474 basmexd 12475 ismgmn0 12612 istps 12824 topontopn 12829 cldrcl 12896 neiss2 12936 |
Copyright terms: Public domain | W3C validator |