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 6619 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
2 | funrel 6374 | . 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 5562 Fun wfun 6351 –1-1-onto→wf1o 6356 |
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 209 df-an 399 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-f1o 6364 |
This theorem is referenced by: f1ococnv1 6645 isores1 7089 weisoeq2 7111 f1oexrnex 7634 ssenen 8693 cantnffval2 9160 hasheqf1oi 13715 cmphaushmeo 22410 cycpmconjs 30800 poimirlem3 34897 f1ocan2fv 35004 ltrncnvnid 37265 brco2f1o 40389 brco3f1o 40390 ntrclsnvobr 40409 ntrclsiex 40410 ntrneiiex 40433 ntrneinex 40434 neicvgel1 40476 |
Copyright terms: Public domain | W3C validator |