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	$$⊢\neg A\in B\leftrightarrow \forall x\in Bx\ne A$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢x\ne A\leftrightarrow \neg x=A$$
2	1	ralbii	$$⊢\forall x\in Bx\ne A\leftrightarrow \forall x\in B\neg x=A$$
3		ralnex	$$⊢\forall x\in B\neg x=A\leftrightarrow \neg \exists x\in Bx=A$$
4	2 3	bitri	$$⊢\forall x\in Bx\ne A\leftrightarrow \neg \exists x\in Bx=A$$
5		risset	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$
6	4 5	xchbinxr	$$⊢\forall x\in Bx\ne A\leftrightarrow \neg A\in B$$
7	6	bicomi	$$⊢\neg A\in B\leftrightarrow \forall x\in Bx\ne A$$