![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-f1 | Unicode version |
Description: Define a one-to-one function. For equivalent definitions see dff12 5785 and dff13 6166. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | wf1 5590 | . 2 |
5 | 1, 2, 3 | wf 5589 | . . 3 |
6 | 3 | ccnv 5003 | . . . 4 |
7 | 6 | wfun 5587 | . . 3 |
8 | 5, 7 | wa 369 | . 2 |
9 | 4, 8 | wb 184 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: f1eq1 5781 f1eq2 5782 f1eq3 5783 nff1 5784 dff12 5785 f1f 5786 f1ss 5791 f1ssr 5792 f1ssres 5793 f1cnvcnv 5794 f1co 5795 dff1o2 5826 f1f1orn 5832 f1imacnv 5837 f10 5852 nvof1o 6186 fun11iun 6760 f11o 6762 f1o2ndf1 6908 tz7.48lem 7125 ssdomg 7581 domunsncan 7637 sbthlem9 7655 fodomr 7688 1sdom 7742 fsuppcolem 7880 fsuppco 7881 enfin1ai 8785 injresinj 11926 isercolllem2 13488 isercoll 13490 ismon2 15129 isepi2 15136 isfth2 15284 fthoppc 15292 odf1o2 16593 frlmlbs 18831 f1lindf 18857 istrl2 24540 wlkntrllem3 24563 spthonepeq 24589 wlkdvspthlem 24609 wlkdvspth 24610 usgra2wlkspthlem1 24619 usgra2wlkspthlem2 24620 cyclnspth 24631 constr3trllem2 24651 4cycl4dv 24667 usg2wotspth 24884 2spontn0vne 24887 eupatrl 24968 rinvf1o 27472 subfacp1lem3 28626 subfacp1lem5 28628 diophrw 30692 usgra2pthspth 32351 spthdifv 32352 usgra2pth 32354 |
Copyright terms: Public domain | W3C validator |