![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-dom | GIF version |
Description: Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6167 and domen 6168. (Contributed by NM, 28-Mar-1998.) |
Ref | Expression |
---|---|
df-dom | ⊢ ≼ = {〈x, y〉 ∣ ∃f f:x–1-1→y} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdom 6156 | . 2 class ≼ | |
2 | vx | . . . . . 6 setvar x | |
3 | 2 | cv 1241 | . . . . 5 class x |
4 | vy | . . . . . 6 setvar y | |
5 | 4 | cv 1241 | . . . . 5 class y |
6 | vf | . . . . . 6 setvar f | |
7 | 6 | cv 1241 | . . . . 5 class f |
8 | 3, 5, 7 | wf1 4842 | . . . 4 wff f:x–1-1→y |
9 | 8, 6 | wex 1378 | . . 3 wff ∃f f:x–1-1→y |
10 | 9, 2, 4 | copab 3808 | . 2 class {〈x, y〉 ∣ ∃f f:x–1-1→y} |
11 | 1, 10 | wceq 1242 | 1 wff ≼ = {〈x, y〉 ∣ ∃f f:x–1-1→y} |
Colors of variables: wff set class |
This definition is referenced by: reldom 6162 brdomg 6165 enssdom 6178 |
Copyright terms: Public domain | W3C validator |