Description: Obsolete version of nelb as of 3-Nov-2024. (Contributed by Thierry Arnoux, 20-Nov-2023) (Proof shortened by SN, 23-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nelbOLD | ⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 ) |
| 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 | ⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 ) |