Metamath Proof Explorer

Theorem nelb

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

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

Proof

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