| 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 6804 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 2 | 1 | ffnd 6737 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Fn wfn 6556 –1-1→wf1 6558 |
| 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-f 6565 df-f1 6566 |
| This theorem is referenced by: f1fun 6806 f1rel 6807 f1dm 6808 f1ssr 6810 f1f1orn 6859 f1elima 7283 f1eqcocnv 7321 domunsncan 9112 f1domfi2 9222 sbthfilem 9238 fodomfir 9368 marypha2 9479 infdifsn 9697 acndom 10091 dfac12lem2 10185 ackbij1 10277 fin23lem32 10384 fin1a2lem5 10444 fin1a2lem6 10445 pwfseqlem1 10698 hashf1lem1 14494 hashf1 14496 kerf1ghm 19265 odf1o2 19591 frlmlbs 21817 f1lindf 21842 2ndcdisj 23464 qtopf1 23824 clwlkclwwlklem2 30019 f1rnen 32639 erdszelem10 35205 pibt2 37418 dihfn 41270 dihcl 41272 dih1dimatlem 41331 dochocss 41368 onsucf1o 43285 cantnfub 43334 cantnfub2 43335 gricushgr 47886 grtrimap 47915 |
| Copyright terms: Public domain | W3C validator |