![]() |
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 6839 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 6655 | . 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 6543 Fn wfn 6544 –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-fn 6552 df-f 6553 df-f1 6554 df-f1o 6556 |
This theorem is referenced by: f1orel 6841 f1oresrab 7136 fveqf1o 7311 isofrlem 7347 isofr 7349 isose 7350 f1opw 7677 xpcomco 9087 dif1en 9185 dif1enOLD 9187 f1opwfi 9382 inlresf 9939 inrresf 9941 djuun 9951 isercolllem2 15648 isercoll 15650 unbenlem 16880 gsumpropd2lem 18642 symgfixf1 19404 tgqtop 23660 hmeontr 23717 reghmph 23741 nrmhmph 23742 tgpconncompeqg 24060 cnheiborlem 24924 dfrelog 26544 dvloglem 26627 logf1o2 26629 axcontlem9 28855 axcontlem10 28856 padct 32583 symgcom 32896 cycpmconjvlem 32954 cycpmconjslem2 32968 madjusmdetlem2 33560 tpr2rico 33644 ballotlemrv 34270 reprpmtf1o 34389 hgt750lemg 34417 subfacp1lem2a 34921 subfacp1lem2b 34922 subfacp1lem5 34925 ismtyres 37412 diaclN 40653 dia1elN 40657 diaintclN 40661 docaclN 40727 dibintclN 40770 cantnf2 42896 sge0f1o 45908 f1oresf1o 46808 uspgrimprop 47357 grimuhgr 47362 |
Copyright terms: Public domain | W3C validator |