Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > funrel | GIF version |
Description: A function is a relation. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
funrel | ⊢ (Fun 𝐴 → Rel 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fun 5125 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 272 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3071 I cid 4210 ◡ccnv 4538 ∘ ccom 4543 Rel wrel 4544 Fun wfun 5117 |
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 5125 |
This theorem is referenced by: 0nelfun 5141 funeu 5148 nfunv 5156 funopg 5157 funssres 5165 funun 5167 fununi 5191 funcnvres2 5198 funimaexg 5207 fnrel 5221 fcoi1 5303 f1orel 5370 funbrfv 5460 funbrfv2b 5466 fvmptss2 5496 mptrcl 5503 elfvmptrab1 5515 funfvbrb 5533 fmptco 5586 funresdfunsnss 5623 elmpocl 5968 mpoxopn0yelv 6136 tfrlem6 6213 funresdfunsndc 6402 pmresg 6570 fundmen 6700 caseinl 6976 caseinr 6977 axaddf 7679 axmulf 7680 hashinfom 10527 structcnvcnv 11978 istopon 12183 eltg4i 12227 eltg3 12229 tg1 12231 tg2 12232 tgclb 12237 lmrcl 12363 |
Copyright terms: Public domain | W3C validator |