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