![]() |
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 6227 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 498 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3859 I cid 5347 ◡ccnv 5442 ∘ ccom 5447 Rel wrel 5448 Fun wfun 6219 |
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 208 df-an 397 df-fun 6227 |
This theorem is referenced by: 0nelfun 6243 funeu 6250 nfunv 6258 funopg 6259 funssres 6268 funun 6270 fununfun 6272 fununi 6299 funcnvres2 6304 fnrel 6324 fcoi1 6420 f1orel 6486 funbrfv 6584 funbrfv2b 6591 funfv2 6618 funfvbrb 6686 fimacnvinrn 6705 fvn0ssdmfun 6707 funopsn 6773 funresdfunsn 6818 funexw 7509 funfv1st2nd 7601 funelss 7602 funeldmdif 7603 wfrrel 7812 tfrlem6 7870 tfr2b 7884 pmresg 8284 fundmen 8431 resfifsupp 8707 rankwflemb 9068 gruima 10070 structcnvcnv 16326 inviso1 16865 setciso 17180 edg0iedg0 26523 edg0usgr 26718 usgr1v0edg 26722 fgreu 30107 cycpmconjvlem 30420 cycpmconjslem2 30435 bnj1379 31719 funen1cnv 31971 fundmpss 32617 funsseq 32619 frrlem6 32737 nolt02o 32808 nosupbnd1 32823 nosupbnd2lem1 32824 nosupbnd2 32825 noetalem2 32827 noetalem3 32828 imageval 33000 imagesset 33023 cocnv 34532 frege124d 39591 frege129d 39593 frege133d 39595 funbrafv 42873 funbrafv2b 42874 funbrafv2 42962 rngciso 43731 rngcisoALTV 43743 ringciso 43782 ringcisoALTV 43806 |
Copyright terms: Public domain | W3C validator |