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 6449 | . 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | |
2 | 1 | simplbi 497 | 1 ⊢ (Fun 𝐴 → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3889 I cid 5490 ◡ccnv 5590 ∘ ccom 5595 Rel wrel 5596 Fun wfun 6441 |
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 396 df-fun 6449 |
This theorem is referenced by: 0nelfun 6469 funeu 6476 nfunv 6484 funopg 6485 funssres 6495 funun 6497 fununfun 6499 fununi 6526 funcnvres2 6531 fnrel 6554 fcoi1 6666 f1orel 6737 funbrfv 6840 funbrfv2b 6847 funfv2 6876 funfvbrb 6948 fimacnvinrn 6969 fvn0ssdmfun 6972 funopsn 7040 funresdfunsn 7081 funexw 7814 funfv1st2nd 7907 funelss 7908 funeldmdif 7909 frrlem6 8127 wfrrelOLD 8165 tfrlem6 8233 tfr2b 8247 pmresg 8678 fundmen 8845 resfifsupp 9184 rankwflemb 9579 gruima 10586 structcnvcnv 16882 inviso1 17506 setciso 17834 edg0iedg0 27453 edg0usgr 27648 usgr1v0edg 27652 fgreu 31037 fressupp 31050 gsumhashmul 31344 cycpmconjvlem 31436 cycpmconjslem2 31450 bnj1379 32838 funen1cnv 33088 fundmpss 33768 funsseq 33770 nolt02o 33926 nogt01o 33927 nosupbnd1 33945 nosupbnd2lem1 33946 nosupbnd2 33947 noinfbnd1 33960 noinfbnd2lem1 33961 noinfbnd2 33962 noetasuplem2 33965 noetasuplem3 33966 noetasuplem4 33967 noetainflem2 33969 imageval 34260 imagesset 34283 cocnv 35911 frege124d 41393 frege129d 41395 frege133d 41397 funbrafv 44690 funbrafv2b 44691 funbrafv2 44779 rngciso 45580 rngcisoALTV 45592 ringciso 45631 ringcisoALTV 45655 ackvalsuc0val 46073 |
Copyright terms: Public domain | W3C validator |