![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1fun | Structured version Visualization version GIF version |
Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1fun | ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1fn 6788 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 6649 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6537 Fn wfn 6538 –1-1→wf1 6540 |
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 396 df-fn 6546 df-f 6547 df-f1 6548 |
This theorem is referenced by: f1cocnv2 6861 f1o2ndf1 8113 fnwelem 8122 f1dmvrnfibi 9342 fsuppco 9403 ackbij1b 10240 fin23lem31 10344 fin1a2lem6 10406 hashimarn 14407 hashf1dmrn 14410 gsumval3lem1 19821 gsumval3lem2 19822 usgrfun 28851 trlsegvdeglem6 29911 ccatf1 32548 cycpmrn 32738 cycpmconjslem2 32750 elhf 35616 |
Copyright terms: Public domain | W3C validator |