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 5180 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
5 | 1, 2, 3 | wf 5179 | . . 3 wff 𝐹:𝐴⟶𝐵 |
6 | 3 | ccnv 4598 | . . . 4 class ◡𝐹 |
7 | 6 | wfun 5177 | . . 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 5383 f1eq2 5384 f1eq3 5385 nff1 5386 dff12 5387 f1f 5388 f1ss 5394 f1ssr 5395 f1ssres 5397 f1cnvcnv 5399 f1co 5400 dff1o2 5432 f1f1orn 5438 f1imacnv 5444 fun11iun 5448 f11o 5460 f10 5461 f1o2ndf1 6188 ssdomg 6736 phplem4dom 6820 sbthlemi9 6922 casefun 7042 casef1 7047 djufun 7061 exmidfodomrlemim 7149 ennnfonelemf1 12305 |
Copyright terms: Public domain | W3C validator |