Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-dom | Structured version Visualization version GIF version |
Description: Define the dominance relation. For an alternate definition see dfdom2 8775. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8759 and domen 8760. (Contributed by NM, 28-Mar-1998.) |
Ref | Expression |
---|---|
df-dom | ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdom 8740 | . 2 class ≼ | |
2 | vx | . . . . . 6 setvar 𝑥 | |
3 | 2 | cv 1538 | . . . . 5 class 𝑥 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1538 | . . . . 5 class 𝑦 |
6 | vf | . . . . . 6 setvar 𝑓 | |
7 | 6 | cv 1538 | . . . . 5 class 𝑓 |
8 | 3, 5, 7 | wf1 6434 | . . . 4 wff 𝑓:𝑥–1-1→𝑦 |
9 | 8, 6 | wex 1782 | . . 3 wff ∃𝑓 𝑓:𝑥–1-1→𝑦 |
10 | 9, 2, 4 | copab 5137 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
11 | 1, 10 | wceq 1539 | 1 wff ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
Colors of variables: wff setvar class |
This definition is referenced by: reldom 8748 brdom2g 8754 brdomgOLD 8756 enssdom 8774 |
Copyright terms: Public domain | W3C validator |