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

Proof

Step	Hyp	Ref	Expression
1		eleq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝑦 ↔ 𝐴 ∈ 𝐵 ) )
2	1	notbid	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝐴 ∈ 𝐵 ) )
3		df-nelbr	⊢ _∉ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ 𝑥 ∈ 𝑦 }
4	2 3	brabga	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 _∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵 ) )