![]() |
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 5232 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 3 | wf 5231 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | ccnv 4643 |
. . . 4
![]() ![]() ![]() |
7 | 6 | wfun 5229 |
. . 3
![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5435 f1eq2 5436 f1eq3 5437 nff1 5438 dff12 5439 f1f 5440 f1ss 5446 f1ssr 5447 f1ssres 5449 f1cnvcnv 5451 f1co 5452 dff1o2 5485 f1f1orn 5491 f1imacnv 5497 fun11iun 5501 f11o 5513 f10 5514 f1o2ndf1 6252 ssdomg 6803 phplem4dom 6889 sbthlemi9 6993 casefun 7113 casef1 7118 djufun 7132 exmidfodomrlemim 7229 4sqlemffi 12427 ennnfonelemf1 12468 |
Copyright terms: Public domain | W3C validator |