![]() |
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 6551 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 496 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3944 I cid 5575 ◡ccnv 5677 ∘ ccom 5682 Rel wrel 5683 Fun wfun 6543 |
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 395 df-fun 6551 |
This theorem is referenced by: 0nelfun 6572 funeu 6579 nfunv 6587 funopg 6588 funssres 6598 funun 6600 fununfun 6602 fununi 6629 funcnvres2 6634 fnrel 6657 fcoi1 6771 f1orel 6841 funbrfv 6947 funbrfv2b 6955 funfv2 6985 funfvbrb 7059 fimacnvinrn 7080 fvn0ssdmfun 7083 funopsn 7157 funresdfunsn 7198 funexw 7956 funfv1st2nd 8051 funelss 8052 funeldmdif 8053 frrlem6 8297 wfrrelOLD 8335 tfrlem6 8403 tfr2b 8417 pmresg 8889 fundmen 9056 resfifsupp 9422 rankwflemb 9818 gruima 10827 structcnvcnv 17125 inviso1 17752 setciso 18083 rngciso 20583 ringciso 20617 nolt02o 27674 nogt01o 27675 nosupbnd1 27693 nosupbnd2lem1 27694 nosupbnd2 27695 noinfbnd1 27708 noinfbnd2lem1 27709 noinfbnd2 27710 noetasuplem2 27713 noetasuplem3 27714 noetasuplem4 27715 noetainflem2 27717 edg0iedg0 28940 edg0usgr 29138 usgr1v0edg 29142 fgreu 32539 fressupp 32550 gsumhashmul 32860 cycpmconjvlem 32954 cycpmconjslem2 32968 bnj1379 34589 funen1cnv 34839 fundmpss 35490 funsseq 35491 imageval 35654 imagesset 35677 cocnv 37326 frege124d 43330 frege129d 43332 frege133d 43334 funbrafv 46673 funbrafv2b 46674 funbrafv2 46762 isubgrvtxuhgr 47333 rngcisoALTV 47522 ringcisoALTV 47556 ackvalsuc0val 47943 |
Copyright terms: Public domain | W3C validator |