Step |
Hyp |
Ref |
Expression |
1 |
|
df-eprel |
⊢ E = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } |
2 |
|
df-id |
⊢ I = { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } |
3 |
1 2
|
ineq12i |
⊢ ( E ∩ I ) = ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } ) |
4 |
|
inopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 ∈ 𝑦 } ∩ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 = 𝑦 } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) } |
5 |
|
nelaneq |
⊢ ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) |
6 |
5
|
gen2 |
⊢ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) |
7 |
|
opab0 |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) ) |
8 |
6 7
|
mpbir |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑦 ∧ 𝑥 = 𝑦 ) } = ∅ |
9 |
3 4 8
|
3eqtri |
⊢ ( E ∩ I ) = ∅ |