Theorem nelb

Description: A definition of -. A e. B . (Contributed by Thierry Arnoux, 20-Nov-2023) (Proof shortened by SN, 23-Jan-2024) (Proof shortened by Wolf Lammen, 3-Nov-2024)

	Ref	Expression
Assertion	nelb	⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝑥 ≠ 𝐴 ↔ ¬ 𝑥 = 𝐴 )
2	1	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 = 𝐴 )
3		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 = 𝐴 ↔ ¬ ∃ 𝑥 ∈ 𝐵 𝑥 = 𝐴 )
4	2 3	bitr2i	⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )
5		risset	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝑥 = 𝐴 )
6	4 5	xchnxbir	⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )