Step |
Hyp |
Ref |
Expression |
1 |
|
df-dm |
⊢ dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝑅 𝑦 } |
2 |
|
nfopab1 |
⊢ Ⅎ 𝑥 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
3 |
2
|
nfeq2 |
⊢ Ⅎ 𝑥 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
4 |
|
nfopab2 |
⊢ Ⅎ 𝑦 { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
5 |
4
|
nfeq2 |
⊢ Ⅎ 𝑦 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } |
6 |
|
df-br |
⊢ ( 𝑥 𝑅 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) |
7 |
|
eleq2 |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → ( 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ↔ 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ) |
8 |
|
opabidw |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 𝜑 ) |
9 |
7 8
|
bitrdi |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → ( 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ↔ 𝜑 ) ) |
10 |
6 9
|
syl5bb |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → ( 𝑥 𝑅 𝑦 ↔ 𝜑 ) ) |
11 |
5 10
|
exbid |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → ( ∃ 𝑦 𝑥 𝑅 𝑦 ↔ ∃ 𝑦 𝜑 ) ) |
12 |
3 11
|
abbid |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → { 𝑥 ∣ ∃ 𝑦 𝑥 𝑅 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝜑 } ) |
13 |
1 12
|
syl5eq |
⊢ ( 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝜑 } ) |