![]() |
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 4923 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
5 | 1, 2, 3 | wf 4922 | . . 3 wff 𝐹:𝐴⟶𝐵 |
6 | 3 | ccnv 4364 | . . . 4 class ◡𝐹 |
7 | 6 | wfun 4920 | . . 3 wff Fun ◡𝐹 |
8 | 5, 7 | wa 102 | . 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) |
9 | 4, 8 | wb 103 | 1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff set class |
This definition is referenced by: f1eq1 5112 f1eq2 5113 f1eq3 5114 nff1 5115 dff12 5116 f1f 5117 f1ss 5122 f1ssr 5123 f1ssres 5124 f1cnvcnv 5125 f1co 5126 dff1o2 5156 f1f1orn 5162 f1imacnv 5168 fun11iun 5172 f11o 5184 f10 5185 f1o2ndf1 5874 ssdomg 6317 phplem4dom 6387 |
Copyright terms: Public domain | W3C validator |