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 5091 | . 2 |
5 | 3, 1 | wfn 5088 | . . 3 |
6 | 3 | crn 4510 | . . . 4 |
7 | 6, 2 | wceq 1316 | . . 3 |
8 | 5, 7 | wa 103 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: foeq1 5311 foeq2 5312 foeq3 5313 nffo 5314 fof 5315 forn 5318 dffo2 5319 dffn4 5321 fores 5324 dff1o2 5340 dff1o3 5341 foimacnv 5353 foun 5354 fconstfvm 5606 dff1o6 5645 fo1st 6023 fo2nd 6024 tposfo2 6132 ctssdc 6966 exmidfodomrlemim 7025 |
Copyright terms: Public domain | W3C validator |