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	|- ( ( A e. V /\ B e. W ) -> ( A e// B <-> A e/ B ) )

Proof

Step	Hyp	Ref	Expression
1		nelbr	|- ( ( A e. V /\ B e. W ) -> ( A e// B <-> -. A e. B ) )
2		df-nel	|- ( A e/ B <-> -. A e. B )
3	1 2	bitr4di	|- ( ( A e. V /\ B e. W ) -> ( A e// B <-> A e/ B ) )