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 6569 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
2 | fnfun 6446 | . 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 6342 Fn wfn 6343 –1-1→wf1 6345 |
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 6351 df-f 6352 df-f1 6353 |
This theorem is referenced by: f1cocnv2 6635 f1o2ndf1 7807 fnwelem 7814 f1dmvrnfibi 8796 fsuppco 8853 ackbij1b 9649 fin23lem31 9753 fin1a2lem6 9815 hashimarn 13789 gsumval3lem1 18954 gsumval3lem2 18955 usgrfun 26870 trlsegvdeglem6 27931 ccatf1 30552 cycpmrn 30712 cycpmconjslem2 30724 hashf1dmrn 32252 elhf 33532 |
Copyright terms: Public domain | W3C validator |