| 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 6776 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
| 2 | funrel 6509 | . 2 ⊢ (Fun 𝐹 → Rel 𝐹) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Rel wrel 5629 Fun wfun 6486 –1-1-onto→wf1o 6491 |
| 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 6494 df-fn 6495 df-f 6496 df-f1 6497 df-f1o 6499 |
| This theorem is referenced by: f1ococnv1 6803 isores1 7280 weisoeq2 7302 f1oexrnex 7869 ssenen 9079 f1oenfirn 9104 cantnffval2 9604 hasheqf1oi 14274 cmphaushmeo 23744 cycpmconjs 33238 poimirlem3 37820 f1ocan2fv 37924 ltrncnvnid 40383 brco2f1o 44269 brco3f1o 44270 ntrclsnvobr 44289 ntrclsiex 44290 ntrneiiex 44313 ntrneinex 44314 neicvgel1 44356 3f1oss1 47317 3f1oss2 47318 |
| Copyright terms: Public domain | W3C validator |