Definition df-nelbr

Description: Define negated membership as binary relation. Analogous to df-eprel (the membership relation). (Contributed by AV, 26-Dec-2021)

	Ref	Expression
Assertion	df-nelbr	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnelbr	⊢ _∉
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	2	cv	⊢ 𝑦
5	3 4	wcel	⊢ 𝑥 ∈ 𝑦
6	5	wn	⊢ ¬ 𝑥 ∈ 𝑦
7	6 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }
8	0 7	wceq	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }