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 5193 | . 2 |
5 | 1, 2, 3 | wf 5192 | . . 3 |
6 | 3 | ccnv 4608 | . . . 4 |
7 | 6 | wfun 5190 | . . 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 5396 f1eq2 5397 f1eq3 5398 nff1 5399 dff12 5400 f1f 5401 f1ss 5407 f1ssr 5408 f1ssres 5410 f1cnvcnv 5412 f1co 5413 dff1o2 5445 f1f1orn 5451 f1imacnv 5457 fun11iun 5461 f11o 5473 f10 5474 f1o2ndf1 6205 ssdomg 6754 phplem4dom 6838 sbthlemi9 6940 casefun 7060 casef1 7065 djufun 7079 exmidfodomrlemim 7171 ennnfonelemf1 12366 |
Copyright terms: Public domain | W3C validator |