Step |
Hyp |
Ref |
Expression |
1 |
|
df-eprel |
⊢ E = { 〈 𝑦 , 𝑥 〉 ∣ 𝑦 ∈ 𝑥 } |
2 |
1
|
cnveqi |
⊢ ◡ E = ◡ { 〈 𝑦 , 𝑥 〉 ∣ 𝑦 ∈ 𝑥 } |
3 |
|
cnvopab |
⊢ ◡ { 〈 𝑦 , 𝑥 〉 ∣ 𝑦 ∈ 𝑥 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 ∈ 𝑥 } |
4 |
2 3
|
eqtri |
⊢ ◡ E = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 ∈ 𝑥 } |
5 |
|
df-eprel |
⊢ E = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } |
6 |
4 5
|
ineq12i |
⊢ ( ◡ E ∩ E ) = ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 ∈ 𝑥 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } ) |
7 |
|
inopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 ∈ 𝑥 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) } |
8 |
6 7
|
eqtri |
⊢ ( ◡ E ∩ E ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) } |
9 |
|
en2lp |
⊢ ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) |
10 |
9
|
gen2 |
⊢ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) |
11 |
|
opab0 |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) |
12 |
10 11
|
mpbir |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) } = ∅ |
13 |
8 12
|
eqtri |
⊢ ( ◡ E ∩ E ) = ∅ |