Theorem nelbrim

Description: If a set is related to another set by the negated membership relation, then it is not a member of the other set. The other direction of the implication is not generally true, because if A is a proper class, then -. A e. B would be true, but not A e// B . (Contributed by AV, 26-Dec-2021)

	Ref	Expression
Assertion	nelbrim	$$⊢A\notin B\to \neg A\in B$$

Proof

Step	Hyp	Ref	Expression
1		df-nelbr	$$⊢\notin =\left\{⟨x,y⟩|\neg x\in y\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\notin$$
3	2	brrelex12i	$$⊢A\notin B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
4		nelbr	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\notin B\leftrightarrow \neg A\in B\right)$$
5	4	biimpd	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\notin B\to \neg A\in B\right)$$
6	3 5	mpcom	$$⊢A\notin B\to \neg A\in B$$