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 e// B -> -. A e. B )

Proof

Step	Hyp	Ref	Expression
1		df-nelbr	|- e// = { <. x , y >. | -. x e. y }
2	1	relopabiv	|- Rel e//
3	2	brrelex12i	|- ( A e// B -> ( A e. _V /\ B e. _V ) )
4		nelbr	|- ( ( A e. _V /\ B e. _V ) -> ( A e// B <-> -. A e. B ) )
5	4	biimpd	|- ( ( A e. _V /\ B e. _V ) -> ( A e// B -> -. A e. B ) )
6	3 5	mpcom	|- ( A e// B -> -. A e. B )