| 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 6563 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 I cid 5577 ◡ccnv 5684 ∘ ccom 5689 Rel wrel 5690 Fun wfun 6555 |
| 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 207 df-an 396 df-fun 6563 |
| This theorem is referenced by: 0nelfun 6584 funeu 6591 nfunv 6599 funopg 6600 funssres 6610 funun 6612 fununfun 6614 fununi 6641 funcnvres2 6646 fnrel 6670 fcoi1 6782 f1orel 6851 funbrfv 6957 funbrfv2b 6966 funfv2 6997 funfvbrb 7071 fimacnvinrn 7091 fvn0ssdmfun 7094 funopsn 7168 funresdfunsn 7209 funexw 7976 funfv1st2nd 8071 funelss 8072 funeldmdif 8073 frrlem6 8316 wfrrelOLD 8354 tfrlem6 8422 tfr2b 8436 pmresg 8910 fundmen 9071 resfifsupp 9437 rankwflemb 9833 gruima 10842 structcnvcnv 17190 inviso1 17810 setciso 18136 rngciso 20638 ringciso 20672 nolt02o 27740 nogt01o 27741 nosupbnd1 27759 nosupbnd2lem1 27760 nosupbnd2 27761 noinfbnd1 27774 noinfbnd2lem1 27775 noinfbnd2 27776 noetasuplem2 27779 noetasuplem3 27780 noetasuplem4 27781 noetainflem2 27783 edg0iedg0 29072 edg0usgr 29270 usgr1v0edg 29274 fgreu 32682 fressupp 32697 gsumhashmul 33064 cycpmconjvlem 33161 cycpmconjslem2 33175 bnj1379 34844 funen1cnv 35102 fundmpss 35767 funsseq 35768 imageval 35931 imagesset 35954 cocnv 37732 frege124d 43774 frege129d 43776 frege133d 43778 funbrafv 47170 funbrafv2b 47171 funbrafv2 47259 isubgrvtxuhgr 47850 rngcisoALTV 48193 ringcisoALTV 48227 ackvalsuc0val 48608 |
| Copyright terms: Public domain | W3C validator |