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 \cap I = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-eprel	$⊢ E = \{⟨x, y⟩ \| x \in y\}$
2		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
3	1 2	ineq12i	$⊢ E \cap I = \{⟨x, y⟩ \| x \in y\} \cap \{⟨x, y⟩ \| x = y\}$
4		inopab	$⊢ \{⟨x, y⟩ \| x \in y\} \cap \{⟨x, y⟩ \| x = y\} = \{⟨x, y⟩ \| (x \in y \land x = y)\}$
5		nelaneq	$⊢ \neg (x \in y \land x = y)$
6	5	gen2	$⊢ \forall x \forall y \neg (x \in y \land x = y)$
7		opab0	$⊢ \{⟨x, y⟩ \| (x \in y \land x = y)\} = \emptyset \leftrightarrow \forall x \forall y \neg (x \in y \land x = y)$
8	6 7	mpbir	$⊢ \{⟨x, y⟩ \| (x \in y \land x = y)\} = \emptyset$
9	3 4 8	3eqtri	$⊢ E \cap I = \emptyset$