This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem epinid0

Description: The membership relation and the identity relation are disjoint. Variable-free version of nelaneq . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022)

Ref Expression
Assertion epinid0 ( E ∩ I ) = ∅

Proof

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 ) = ∅