Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-f1 | Unicode version |
Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | wf1 4899 | . 2 |
5 | 1, 2, 3 | wf 4898 | . . 3 |
6 | 3 | ccnv 4344 | . . . 4 |
7 | 6 | wfun 4896 | . . 3 |
8 | 5, 7 | wa 97 | . 2 |
9 | 4, 8 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5087 f1eq2 5088 f1eq3 5089 nff1 5090 dff12 5091 f1f 5092 f1ss 5097 f1ssr 5098 f1ssres 5099 f1cnvcnv 5100 f1co 5101 dff1o2 5131 f1f1orn 5137 f1imacnv 5143 fun11iun 5147 f11o 5159 f10 5160 f1o2ndf1 5849 ssdomg 6258 phplem4dom 6324 |
Copyright terms: Public domain | W3C validator |