![]() |
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 6358 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
2 | funrel 6118 | . 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 5317 Fun wfun 6095 –1-1-onto→wf1o 6100 |
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 199 df-an 386 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-f1o 6108 |
This theorem is referenced by: f1ococnv1 6384 isores1 6812 weisoeq2 6834 f1oexrnex 7350 ssenen 8376 cantnffval2 8842 hasheqf1oi 13392 cmphaushmeo 21932 poimirlem3 33901 f1ocan2fv 34010 ltrncnvnid 36148 brco2f1o 39112 brco3f1o 39113 ntrclsnvobr 39132 ntrclsiex 39133 ntrneiiex 39156 ntrneinex 39157 neicvgel1 39199 |
Copyright terms: Public domain | W3C validator |