Theorem nelbrnel

Description: A set is related to another set by the negated membership relation iff it is not a member of the other set. (Contributed by AV, 26-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nelbr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\notin B\leftrightarrow \neg A\in B\right)$$
2		df-nel	$$⊢A\notin B\leftrightarrow \neg A\in B$$
3	1 2	bitr4di	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\notin B\leftrightarrow A\notin B\right)$$