![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1fn | Structured version Visualization version GIF version |
Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1fn | ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1f 6139 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 6083 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 5921 ⟶wf 5922 –1-1→wf1 5923 |
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 197 df-an 385 df-f 5930 df-f1 5931 |
This theorem is referenced by: f1fun 6141 f1rel 6142 f1dm 6143 f1ssr 6145 f1f1orn 6186 f1elima 6560 f1eqcocnv 6596 domunsncan 8101 marypha2 8386 infdifsn 8592 acndom 8912 dfac12lem2 9004 ackbij1 9098 fin23lem32 9204 fin1a2lem5 9264 fin1a2lem6 9265 pwfseqlem1 9518 hashf1lem1 13277 hashf1 13279 odf1o2 18034 kerf1hrm 18791 frlmlbs 20184 f1lindf 20209 2ndcdisj 21307 qtopf1 21667 clwlkclwwlklem2 26966 erdszelem10 31308 dihfn 36874 dihcl 36876 dih1dimatlem 36935 dochocss 36972 |
Copyright terms: Public domain | W3C validator |