Theorem nelbOLDOLD

Description: Obsolete version of nelb as of 23-Jan-2024. (Contributed by Thierry Arnoux, 20-Nov-2023) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nelbOLDOLD	$$⊢\neg A\in B\leftrightarrow \forall x\in Bx\ne A$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in B\neg x=A\leftrightarrow \forall x\left(x\in B\to \neg x=A\right)$$
2		df-ne	$$⊢x\ne A\leftrightarrow \neg x=A$$
3	2	ralbii	$$⊢\forall x\in Bx\ne A\leftrightarrow \forall x\in B\neg x=A$$
4		dfclel	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$
5	4	notbii	$$⊢\neg A\in B\leftrightarrow \neg \exists x\left(x=A\wedge x\in B\right)$$
6		alnex	$$⊢\forall x\neg \left(x=A\wedge x\in B\right)\leftrightarrow \neg \exists x\left(x=A\wedge x\in B\right)$$
7		imnan	$$⊢\left(x\in B\to \neg x=A\right)\leftrightarrow \neg \left(x\in B\wedge x=A\right)$$
8		ancom	$$⊢\left(x\in B\wedge x=A\right)\leftrightarrow \left(x=A\wedge x\in B\right)$$
9	8	notbii	$$⊢\neg \left(x\in B\wedge x=A\right)\leftrightarrow \neg \left(x=A\wedge x\in B\right)$$
10	7 9	bitr2i	$$⊢\neg \left(x=A\wedge x\in B\right)\leftrightarrow \left(x\in B\to \neg x=A\right)$$
11	10	albii	$$⊢\forall x\neg \left(x=A\wedge x\in B\right)\leftrightarrow \forall x\left(x\in B\to \neg x=A\right)$$
12	5 6 11	3bitr2i	$$⊢\neg A\in B\leftrightarrow \forall x\left(x\in B\to \neg x=A\right)$$
13	1 3 12	3bitr4ri	$$⊢\neg A\in B\leftrightarrow \forall x\in Bx\ne A$$