Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1ofun | Structured version Visualization version GIF version |
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1ofun | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ofn 6610 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 6447 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6343 Fn wfn 6344 –1-1-onto→wf1o 6348 |
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 208 df-an 397 df-fn 6352 df-f 6353 df-f1 6354 df-f1o 6356 |
This theorem is referenced by: f1orel 6612 f1oresrab 6882 fveqf1o 7049 isofrlem 7082 isofr 7084 isose 7085 f1opw 7390 xpcomco 8596 f1opwfi 8817 inlresf 9332 inrresf 9334 djuun 9344 isercolllem2 15012 isercoll 15014 unbenlem 16234 gsumpropd2lem 17879 symgfixf1 18496 tgqtop 22250 hmeontr 22307 reghmph 22331 nrmhmph 22332 tgpconncompeqg 22649 cnheiborlem 23487 dfrelog 25076 dvloglem 25158 logf1o2 25160 axcontlem9 26686 axcontlem10 26687 padct 30382 symgcom 30655 cycpmconjvlem 30711 cycpmconjslem2 30725 madjusmdetlem2 30993 tpr2rico 31055 ballotlemrv 31677 reprpmtf1o 31797 hgt750lemg 31825 subfacp1lem2a 32325 subfacp1lem2b 32326 subfacp1lem5 32329 ismtyres 34969 diaclN 38068 dia1elN 38072 diaintclN 38076 docaclN 38142 dibintclN 38185 sge0f1o 42545 f1oresf1o 43370 |
Copyright terms: Public domain | W3C validator |