![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-f1 | Unicode version |
Description: Define a one-to-one function. 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 4842 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 3 | wf 4841 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | ccnv 4287 |
. . . 4
![]() ![]() ![]() |
7 | 6 | wfun 4839 |
. . 3
![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 97 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5030 f1eq2 5031 f1eq3 5032 nff1 5033 dff12 5034 f1f 5035 f1ss 5040 f1ssr 5041 f1ssres 5042 f1cnvcnv 5043 f1co 5044 dff1o2 5074 f1f1orn 5080 f1imacnv 5086 fun11iun 5090 f11o 5102 f10 5103 f1o2ndf1 5791 ssdomg 6194 |
Copyright terms: Public domain | W3C validator |