dfnelbr2

Description: Alternate definition of the negated membership as binary relation. (Proposed by BJ, 27-Dec-2021.) (Contributed by AV, 27-Dec-2021)

		Ref	Expression
	Assertion	dfnelbr2	$⊢ \notin = (V \times V) ∖ E$

Step	Hyp	Ref	Expression
1		difopab	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} ∖ \{⟨x, y⟩ \| x \in y\} = \{⟨x, y⟩ \| ((x \in V \land y \in V) \land \neg x \in y)\}$
2		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
3		df-eprel	$⊢ E = \{⟨x, y⟩ \| x \in y\}$
4	2 3	difeq12i	$⊢ (V \times V) ∖ E = \{⟨x, y⟩ \| (x \in V \land y \in V)\} ∖ \{⟨x, y⟩ \| x \in y\}$
5		df-nelbr	$⊢ \notin = \{⟨x, y⟩ \| \neg x \in y\}$
6		vex	$⊢ x \in V$
7		vex	$⊢ y \in V$
8	6 7	pm3.2i	$⊢ (x \in V \land y \in V)$
9	8	biantrur	$⊢ \neg x \in y \leftrightarrow ((x \in V \land y \in V) \land \neg x \in y)$
10	9	opabbii	$⊢ \{⟨x, y⟩ \| \neg x \in y\} = \{⟨x, y⟩ \| ((x \in V \land y \in V) \land \neg x \in y)\}$
11	5 10	eqtri	$⊢ \notin = \{⟨x, y⟩ \| ((x \in V \land y \in V) \land \neg x \in y)\}$
12	1 4 11	3eqtr4ri	$⊢ \notin = (V \times V) ∖ E$

Metamath Proof Explorer