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