![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > f1fn | Unicode version |
Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1fn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1f 5602 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ffn 5554 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem is referenced by: f1fun 5604 f1rel 5605 f1dm 5606 f1ssr 5608 f1f1orn 5648 f1elima 5972 f1eqcocnv 5991 domunsncan 7171 marypha2 7406 infdifsn 7571 acndom 7892 dfac12lem2 7984 ackbij1 8078 fin23lem32 8184 fin1a2lem5 8244 fin1a2lem6 8245 pwfseqlem1 8493 hashf1lem1 11663 hashf1 11665 odf1o2 15166 2ndcdisj 17476 qtopf1 17805 usgraedgrn 21358 kerf1hrm 24219 erdszelem10 24843 frlmlbs 27121 f1lindf 27164 usgfidegfi 28094 dihfn 31755 dihcl 31757 dih1dimatlem 31816 dochocss 31853 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 df-an 361 df-f 5421 df-f1 5422 |
Copyright terms: Public domain | W3C validator |