Metamath Proof Explorer


Theorem nelbOLD

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
|- ( -. 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 bitri
 |-  ( A. x e. B x =/= A <-> -. E. x e. B x = A )
5 risset
 |-  ( A e. B <-> E. x e. B x = A )
6 4 5 xchbinxr
 |-  ( A. x e. B x =/= A <-> -. A e. B )
7 6 bicomi
 |-  ( -. A e. B <-> A. x e. B x =/= A )