![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-fo | Unicode version |
Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-fo |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wfo 5226 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 1 | wfn 5223 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3 | crn 4639 |
. . . 4
![]() ![]() ![]() |
7 | 6, 2 | wceq 1363 |
. . 3
![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: foeq1 5446 foeq2 5447 foeq3 5448 nffo 5449 fof 5450 forn 5453 dffo2 5454 dffn4 5456 fores 5459 dff1o2 5478 dff1o3 5479 foimacnv 5491 foun 5492 fconstfvm 5747 dff1o6 5790 fo1st 6171 fo2nd 6172 tposfo2 6281 ctssdc 7125 exmidfodomrlemim 7213 reeff1o 14465 |
Copyright terms: Public domain | W3C validator |