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) (Proof shortened by Wolf Lammen, 3-Nov-2024)

Ref Expression
Assertion nelb
|- ( -. A e. B <-> A. x e. B x =/= A )

Proof

Step Hyp Ref Expression
1 df-ne
 |-  ( x =/= A <-> -. x = A )
2 1 ralbii
 |-  ( A. x e. B x =/= A <-> A. x e. B -. x = A )
3 ralnex
 |-  ( A. x e. B -. x = A <-> -. E. x e. B x = A )
4 2 3 bitr2i
 |-  ( -. E. x e. B x = A <-> A. x e. B x =/= A )
5 risset
 |-  ( A e. B <-> E. x e. B x = A )
6 4 5 xchnxbir
 |-  ( -. A e. B <-> A. x e. B x =/= A )