This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification 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 ⊢ ¬ A ∈ B ↔ ∀ x ∈ B x ≠ A
Proof
Step
Hyp
Ref
Expression
1
df-ne ⊢ x ≠ A ↔ ¬ x = A
2
1
ralbii ⊢ ∀ x ∈ B x ≠ A ↔ ∀ x ∈ B ¬ x = A
3
ralnex ⊢ ∀ x ∈ B ¬ x = A ↔ ¬ ∃ x ∈ B x = A
4
2 3
bitr2i ⊢ ¬ ∃ x ∈ B x = A ↔ ∀ x ∈ B x ≠ A
5
risset ⊢ A ∈ B ↔ ∃ x ∈ B x = A
6
4 5
xchnxbir ⊢ ¬ A ∈ B ↔ ∀ x ∈ B x ≠ A