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 5180 | . 2 |
5 | 3, 1 | wfn 5177 | . . 3 |
6 | 3 | crn 4599 | . . . 4 |
7 | 6, 2 | wceq 1342 | . . 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 5400 foeq2 5401 foeq3 5402 nffo 5403 fof 5404 forn 5407 dffo2 5408 dffn4 5410 fores 5413 dff1o2 5431 dff1o3 5432 foimacnv 5444 foun 5445 fconstfvm 5697 dff1o6 5738 fo1st 6117 fo2nd 6118 tposfo2 6226 ctssdc 7069 exmidfodomrlemim 7148 reeff1o 13241 |
Copyright terms: Public domain | W3C validator |