Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funrel | Structured version Visualization version 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 5806 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 475 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3540 I cid 4948 ◡ccnv 5037 ∘ ccom 5042 Rel wrel 5043 Fun wfun 5798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-fun 5806 |
This theorem is referenced by: funeu 5828 nfunv 5835 funopg 5836 funssres 5844 funun 5846 fununfun 5848 fununi 5878 funcnvres2 5883 fnrel 5903 fcoi1 5991 f1orel 6053 funbrfv 6144 funbrfv2b 6150 funfv2 6176 funfvbrb 6238 fimacnvinrn 6256 fvn0ssdmfun 6258 funopsn 6319 funresdfunsn 6360 wfrrel 7307 tfrlem6 7365 tfr2b 7379 pmresg 7771 fundmen 7916 resfifsupp 8186 rankwflemb 8539 gruima 9503 structcnvcnv 15706 inviso1 16249 setciso 16564 pmtrsn 17762 00lsp 18802 edg0iedg0 25800 constr3pthlem1 26183 0eusgraiff0rgracl 26468 fmptcof2 28839 fgreu 28854 bnj1379 30155 fundmpss 30910 funsseq 30912 frrlem5b 31029 frrlem6 31033 nofulllem3 31103 nofulllem5 31105 imageval 31207 imagesset 31230 cocnv 32690 frege124d 37072 frege129d 37074 frege133d 37076 funbrafv 39887 funbrafv2b 39888 edg0usgr 40479 usgr1v0edg 40483 rngciso 41774 rngcisoALTV 41786 ringciso 41825 ringcisoALTV 41849 |
Copyright terms: Public domain | W3C validator |