![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-f1o | Unicode version |
Description: Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wf1o 5217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 3 | wf1 5215 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 3 | wfo 5216 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
7 | 5, 6 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: f1oeq1 5451 f1oeq2 5452 f1oeq3 5453 nff1o 5461 f1of1 5462 dff1o2 5468 dff1o5 5472 f1oco 5486 fo00 5499 dff1o6 5779 fcof1o 5792 tposf1o2 6273 cnref1o 9652 1arith 12367 xpsff1o 12773 reeff1o 14233 ioocosf1o 14314 |
Copyright terms: Public domain | W3C validator |