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	$$⊢\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	bitr2i	$$⊢\neg \exists x\in Bx=A\leftrightarrow \forall x\in Bx\ne A$$
5		risset	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$
6	4 5	xchnxbir	$$⊢\neg A\in B\leftrightarrow \forall x\in Bx\ne A$$