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 6670 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6601 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fn wfn 6428 –1-1→wf1 6430 |
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 397 df-f 6437 df-f1 6438 |
This theorem is referenced by: f1fun 6672 f1rel 6673 f1dm 6674 f1dmOLD 6675 f1ssr 6677 f1f1orn 6727 f1elima 7136 f1eqcocnv 7173 f1eqcocnvOLD 7174 domunsncan 8859 f1domfi2 8968 sbthfilem 8984 marypha2 9198 infdifsn 9415 acndom 9807 dfac12lem2 9900 ackbij1 9994 fin23lem32 10100 fin1a2lem5 10160 fin1a2lem6 10161 pwfseqlem1 10414 hashf1lem1 14168 hashf1lem1OLD 14169 hashf1 14171 odf1o2 19178 kerf1ghm 19987 frlmlbs 21004 f1lindf 21029 2ndcdisj 22607 qtopf1 22967 clwlkclwwlklem2 28364 f1rnen 30964 erdszelem10 33162 pibt2 35588 dihfn 39282 dihcl 39284 dih1dimatlem 39343 dochocss 39380 isomushgr 45278 |
Copyright terms: Public domain | W3C validator |