Theorem dfdif3

Description: Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022) (Proof shortened by SN, 15-Aug-2025)

	Ref	Expression
Assertion	dfdif3	$$⊢A\setminus B=\left\{x\in A|\forall y\in Bx\ne y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfdif2	$$⊢A\setminus B=\left\{x\in A|\neg x\in B\right\}$$
2		nelb	$$⊢\neg x\in B\leftrightarrow \forall y\in By\ne x$$
3		necom	$$⊢y\ne x\leftrightarrow x\ne y$$
4	3	ralbii	$$⊢\forall y\in By\ne x\leftrightarrow \forall y\in Bx\ne y$$
5	2 4	bitri	$$⊢\neg x\in B\leftrightarrow \forall y\in Bx\ne y$$
6	1 5	rabbieq	$$⊢A\setminus B=\left\{x\in A|\forall y\in Bx\ne y\right\}$$