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 6575 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6506 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 6335 –1-1→wf1 6337 |
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 210 df-an 400 df-f 6344 df-f1 6345 |
This theorem is referenced by: f1fun 6577 f1rel 6578 f1dm 6579 f1dmOLD 6580 f1ssr 6582 f1f1orn 6630 f1elima 7033 f1eqcocnv 7069 f1eqcocnvOLD 7070 domunsncan 8667 marypha2 8977 infdifsn 9194 acndom 9552 dfac12lem2 9645 ackbij1 9739 fin23lem32 9845 fin1a2lem5 9905 fin1a2lem6 9906 pwfseqlem1 10159 hashf1lem1 13907 hashf1lem1OLD 13908 hashf1 13910 odf1o2 18817 kerf1ghm 19618 frlmlbs 20614 f1lindf 20639 2ndcdisj 22208 qtopf1 22568 clwlkclwwlklem2 27937 f1rnen 30538 erdszelem10 32733 pibt2 35208 dihfn 38902 dihcl 38904 dih1dimatlem 38963 dochocss 39000 isomushgr 44804 |
Copyright terms: Public domain | W3C validator |