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