![]() |
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 5076 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 3 | wf 5075 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | ccnv 4496 |
. . . 4
![]() ![]() ![]() |
7 | 6 | wfun 5073 |
. . 3
![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5279 f1eq2 5280 f1eq3 5281 nff1 5282 dff12 5283 f1f 5284 f1ss 5290 f1ssr 5291 f1ssres 5293 f1cnvcnv 5295 f1co 5296 dff1o2 5326 f1f1orn 5332 f1imacnv 5338 fun11iun 5342 f11o 5354 f10 5355 f1o2ndf1 6077 ssdomg 6624 phplem4dom 6707 sbthlemi9 6803 casefun 6920 casef1 6925 djufun 6939 exmidfodomrlemim 7002 ennnfonelemf1 11770 |
Copyright terms: Public domain | W3C validator |