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 5120 | . 2 |
5 | 1, 2, 3 | wf 5119 | . . 3 |
6 | 3 | ccnv 4538 | . . . 4 |
7 | 6 | wfun 5117 | . . 3 |
8 | 5, 7 | wa 103 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5323 f1eq2 5324 f1eq3 5325 nff1 5326 dff12 5327 f1f 5328 f1ss 5334 f1ssr 5335 f1ssres 5337 f1cnvcnv 5339 f1co 5340 dff1o2 5372 f1f1orn 5378 f1imacnv 5384 fun11iun 5388 f11o 5400 f10 5401 f1o2ndf1 6125 ssdomg 6672 phplem4dom 6756 sbthlemi9 6853 casefun 6970 casef1 6975 djufun 6989 exmidfodomrlemim 7057 ennnfonelemf1 11931 |
Copyright terms: Public domain | W3C validator |