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	⊢ ( 𝐴 _∉ 𝐵 → ¬ 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-nelbr	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }
2	1	relopabiv	⊢ Rel _∉
3	2	brrelex12i	⊢ ( 𝐴 _∉ 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4		nelbr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 _∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵 ) )
5	4	biimpd	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 _∉ 𝐵 → ¬ 𝐴 ∈ 𝐵 ) )
6	3 5	mpcom	⊢ ( 𝐴 _∉ 𝐵 → ¬ 𝐴 ∈ 𝐵 )