| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1orel | Structured version Visualization version GIF version | ||
| Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.) |
| Ref | Expression |
|---|---|
| f1orel | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1ofun 6812 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
| 2 | funrel 6542 | . 2 ⊢ (Fun 𝐹 → Rel 𝐹) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Rel wrel 5657 Fun wfun 6519 –1-1-onto→wf1o 6524 |
| 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 210 df-an 401 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-f1o 6532 |
| This theorem is referenced by: f1ococnv1 6840 isores1 7322 weisoeq2 7344 f1oexrnex 7912 ssenen 9127 f1oenfirn 9152 cantnffval2 9652 hasheqf1oi 14378 cmphaushmeo 23918 cycpmconjs 33389 f1ocan2fv 38238 ltrncnvnid 40763 brco2f1o 44620 brco3f1o 44621 ntrclsnvobr 44640 ntrclsiex 44641 ntrneiiex 44664 ntrneinex 44665 neicvgel1 44707 3f1oss1 47667 3f1oss2 47668 |
| Copyright terms: Public domain | W3C validator |