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 5121 | . 2 |
5 | 3, 1 | wfn 5118 | . . 3 |
6 | 3 | crn 4540 | . . . 4 |
7 | 6, 2 | wceq 1331 | . . 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 5341 foeq2 5342 foeq3 5343 nffo 5344 fof 5345 forn 5348 dffo2 5349 dffn4 5351 fores 5354 dff1o2 5372 dff1o3 5373 foimacnv 5385 foun 5386 fconstfvm 5638 dff1o6 5677 fo1st 6055 fo2nd 6056 tposfo2 6164 ctssdc 6998 exmidfodomrlemim 7057 |
Copyright terms: Public domain | W3C validator |