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	$$⊢\notin =\left\{⟨x,y⟩|\neg x\in y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnelbr	$$class\notin$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	2	cv	$$setvary$$
5	3 4	wcel	$$wffx\in y$$
6	5	wn	$$wff\neg x\in y$$
7	6 1 2	copab	$$class\left\{⟨x,y⟩|\neg x\in y\right\}$$
8	0 7	wceq	$$wff\notin =\left\{⟨x,y⟩|\neg x\in y\right\}$$