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 5195 | . 2 |
5 | 1, 2, 3 | wf 5194 | . . 3 |
6 | 3 | ccnv 4610 | . . . 4 |
7 | 6 | wfun 5192 | . . 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 5398 f1eq2 5399 f1eq3 5400 nff1 5401 dff12 5402 f1f 5403 f1ss 5409 f1ssr 5410 f1ssres 5412 f1cnvcnv 5414 f1co 5415 dff1o2 5447 f1f1orn 5453 f1imacnv 5459 fun11iun 5463 f11o 5475 f10 5476 f1o2ndf1 6207 ssdomg 6756 phplem4dom 6840 sbthlemi9 6942 casefun 7062 casef1 7067 djufun 7081 exmidfodomrlemim 7178 ennnfonelemf1 12373 |
Copyright terms: Public domain | W3C validator |