| 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 6849 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
| 2 | fnfun 6668 | . 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 6555 Fn wfn 6556 –1-1-onto→wf1o 6560 |
| 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 207 df-an 396 df-fn 6564 df-f 6565 df-f1 6566 df-f1o 6568 |
| This theorem is referenced by: f1orel 6851 f1oresrab 7147 fveqf1o 7322 isofrlem 7360 isofr 7362 isose 7363 f1opw 7689 xpcomco 9102 dif1en 9200 dif1enOLD 9202 f1opwfi 9396 inlresf 9954 inrresf 9956 djuun 9966 isercolllem2 15702 isercoll 15704 unbenlem 16946 gsumpropd2lem 18692 symgfixf1 19455 tgqtop 23720 hmeontr 23777 reghmph 23801 nrmhmph 23802 tgpconncompeqg 24120 cnheiborlem 24986 dfrelog 26607 dvloglem 26690 logf1o2 26692 axcontlem9 28987 axcontlem10 28988 padct 32731 symgcom 33103 cycpmconjvlem 33161 cycpmconjslem2 33175 madjusmdetlem2 33827 tpr2rico 33911 ballotlemrv 34522 reprpmtf1o 34641 hgt750lemg 34669 subfacp1lem2a 35185 subfacp1lem2b 35186 subfacp1lem5 35189 ismtyres 37815 diaclN 41052 dia1elN 41056 diaintclN 41060 docaclN 41126 dibintclN 41169 cantnf2 43338 sge0f1o 46397 f1oresf1o 47302 uspgrimprop 47873 grimuhgr 47878 uhgrimisgrgric 47899 |
| Copyright terms: Public domain | W3C validator |