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 6052 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
2 | funrel 5821 | . 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 5043 Fun wfun 5798 –1-1-onto→wf1o 5803 |
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 196 df-an 385 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-f1o 5811 |
This theorem is referenced by: f1ococnv1 6078 isores1 6484 weisoeq2 6506 f1oexrnex 7008 ssenen 8019 cantnffval2 8475 hasheqf1oi 13002 hasheqf1oiOLD 13003 cmphaushmeo 21413 poimirlem3 32582 f1ocan2fv 32692 ltrncnvnid 34431 brco2f1o 37350 brco3f1o 37351 ntrclsnvobr 37370 ntrclsiex 37371 ntrneiiex 37394 ntrneinex 37395 neicvgel1 37437 |
Copyright terms: Public domain | W3C validator |