![]() |
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 6840 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
2 | funrel 6571 | . 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 5683 Fun wfun 6543 –1-1-onto→wf1o 6548 |
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 206 df-an 395 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-f1o 6556 |
This theorem is referenced by: f1ococnv1 6867 isores1 7341 weisoeq2 7363 f1oexrnex 7935 ssenen 9176 f1oenfirn 9208 cantnffval2 9720 hasheqf1oi 14346 cmphaushmeo 23748 cycpmconjs 32969 poimirlem3 37227 f1ocan2fv 37331 ltrncnvnid 39730 brco2f1o 43604 brco3f1o 43605 ntrclsnvobr 43624 ntrclsiex 43625 ntrneiiex 43648 ntrneinex 43649 neicvgel1 43691 |
Copyright terms: Public domain | W3C validator |