![]() |
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 4967 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 1 | wfn 4964 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3 | crn 4402 |
. . . 4
![]() ![]() ![]() |
7 | 6, 2 | wceq 1285 |
. . 3
![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 102 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: foeq1 5177 foeq2 5178 foeq3 5179 nffo 5180 fof 5181 forn 5184 dffo2 5185 dffn4 5187 fores 5190 dff1o2 5206 dff1o3 5207 foimacnv 5219 foun 5220 fconstfvm 5455 dff1o6 5495 fo1st 5863 fo2nd 5864 tposfo2 5964 exmidfodomrlemim 6730 |
Copyright terms: Public domain | W3C validator |