Theorem nelbr

Description: The binary relation of a set not being a member of another set. (Contributed by AV, 26-Dec-2021)

	Ref	Expression
Assertion	nelbr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\notin B\leftrightarrow \neg A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x\in y\leftrightarrow A\in B\right)$$
2	1	notbid	$$⊢\left(x=A\wedge y=B\right)\to \left(\neg x\in y\leftrightarrow \neg A\in B\right)$$
3		df-nelbr	$$⊢\notin =\left\{⟨x,y⟩|\neg x\in y\right\}$$
4	2 3	brabga	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\notin B\leftrightarrow \neg A\in B\right)$$