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 6668 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) | |
2 | funrel 6402 | . 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 5561 Fun wfun 6379 –1-1-onto→wf1o 6384 |
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 210 df-an 400 df-fun 6387 df-fn 6388 df-f 6389 df-f1 6390 df-f1o 6392 |
This theorem is referenced by: f1ococnv1 6694 isores1 7148 weisoeq2 7170 f1oexrnex 7710 ssenen 8825 f1oenfirn 8865 cantnffval2 9315 hasheqf1oi 13923 cmphaushmeo 22702 cycpmconjs 31147 poimirlem3 35522 f1ocan2fv 35627 ltrncnvnid 37883 brco2f1o 41327 brco3f1o 41328 ntrclsnvobr 41347 ntrclsiex 41348 ntrneiiex 41371 ntrneinex 41372 neicvgel1 41414 |
Copyright terms: Public domain | W3C validator |