Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-f1 | GIF 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 | ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wf1 5090 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
5 | 1, 2, 3 | wf 5089 | . . 3 wff 𝐹:𝐴⟶𝐵 |
6 | 3 | ccnv 4508 | . . . 4 class ◡𝐹 |
7 | 6 | wfun 5087 | . . 3 wff Fun ◡𝐹 |
8 | 5, 7 | wa 103 | . 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) |
9 | 4, 8 | wb 104 | 1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5293 f1eq2 5294 f1eq3 5295 nff1 5296 dff12 5297 f1f 5298 f1ss 5304 f1ssr 5305 f1ssres 5307 f1cnvcnv 5309 f1co 5310 dff1o2 5340 f1f1orn 5346 f1imacnv 5352 fun11iun 5356 f11o 5368 f10 5369 f1o2ndf1 6093 ssdomg 6640 phplem4dom 6724 sbthlemi9 6821 casefun 6938 casef1 6943 djufun 6957 exmidfodomrlemim 7025 ennnfonelemf1 11842 |
Copyright terms: Public domain | W3C validator |