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 6434 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 498 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3892 I cid 5489 ◡ccnv 5589 ∘ ccom 5594 Rel wrel 5595 Fun wfun 6426 |
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 206 df-an 397 df-fun 6434 |
This theorem is referenced by: 0nelfun 6450 funeu 6457 nfunv 6465 funopg 6466 funssres 6476 funun 6478 fununfun 6480 fununi 6507 funcnvres2 6512 fnrel 6533 fcoi1 6646 f1orel 6717 funbrfv 6817 funbrfv2b 6824 funfv2 6853 funfvbrb 6925 fimacnvinrn 6946 fvn0ssdmfun 6949 funopsn 7017 funresdfunsn 7058 funexw 7788 funfv1st2nd 7880 funelss 7881 funeldmdif 7882 frrlem6 8098 wfrrelOLD 8136 tfrlem6 8204 tfr2b 8218 pmresg 8641 fundmen 8804 resfifsupp 9134 rankwflemb 9552 gruima 10559 structcnvcnv 16852 inviso1 17476 setciso 17804 edg0iedg0 27423 edg0usgr 27618 usgr1v0edg 27622 fgreu 31005 fressupp 31018 gsumhashmul 31312 cycpmconjvlem 31404 cycpmconjslem2 31418 bnj1379 32806 funen1cnv 33056 fundmpss 33736 funsseq 33738 nolt02o 33894 nogt01o 33895 nosupbnd1 33913 nosupbnd2lem1 33914 nosupbnd2 33915 noinfbnd1 33928 noinfbnd2lem1 33929 noinfbnd2 33930 noetasuplem2 33933 noetasuplem3 33934 noetasuplem4 33935 noetainflem2 33937 imageval 34228 imagesset 34251 cocnv 35879 frege124d 41339 frege129d 41341 frege133d 41343 funbrafv 44618 funbrafv2b 44619 funbrafv2 44707 rngciso 45509 rngcisoALTV 45521 ringciso 45560 ringcisoALTV 45584 ackvalsuc0val 46002 |
Copyright terms: Public domain | W3C validator |