Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-f1o | Unicode version |
Description: Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | wf1o 5181 | . 2 |
5 | 1, 2, 3 | wf1 5179 | . . 3 |
6 | 1, 2, 3 | wfo 5180 | . . 3 |
7 | 5, 6 | wa 103 | . 2 |
8 | 4, 7 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: f1oeq1 5415 f1oeq2 5416 f1oeq3 5417 nff1o 5424 f1of1 5425 dff1o2 5431 dff1o5 5435 f1oco 5449 fo00 5462 dff1o6 5738 fcof1o 5751 tposf1o2 6229 cnref1o 9579 reeff1o 13241 ioocosf1o 13322 |
Copyright terms: Public domain | W3C validator |