dfdif3

Description: Alternate definition of class difference. (Contributed by BJ and Jim Kingdon, 16-Jun-2022)

		Ref	Expression
	Assertion	dfdif3	$⊢ A ∖ B = \{x \in A \| \forall y \in B x \neq y\}$

Proof

Step	Hyp	Ref	Expression
1		dfdif2	$⊢ A ∖ B = \{x \in A \| \neg x \in B\}$
2		ax6ev	$⊢ \exists y y = x$
3	2	biantrur	$⊢ \neg x \in B \leftrightarrow (\exists y y = x \land \neg x \in B)$
4		19.41v	$⊢ \exists y (y = x \land \neg x \in B) \leftrightarrow (\exists y y = x \land \neg x \in B)$
5	3 4	bitr4i	$⊢ \neg x \in B \leftrightarrow \exists y (y = x \land \neg x \in B)$
6		sbalex	$⊢ \exists y (y = x \land \neg x \in B) \leftrightarrow \forall y (y = x \to \neg x \in B)$
7		equcom	$⊢ y = x \leftrightarrow x = y$
8	7	imbi1i	$⊢ (y = x \to \neg x \in B) \leftrightarrow (x = y \to \neg x \in B)$
9		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
10	9	notbid	$⊢ x = y \to (\neg x \in B \leftrightarrow \neg y \in B)$
11	10	pm5.74i	$⊢ (x = y \to \neg x \in B) \leftrightarrow (x = y \to \neg y \in B)$
12		con2b	$⊢ (x = y \to \neg y \in B) \leftrightarrow (y \in B \to \neg x = y)$
13		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
14	13	bicomi	$⊢ \neg x = y \leftrightarrow x \neq y$
15	14	imbi2i	$⊢ (y \in B \to \neg x = y) \leftrightarrow (y \in B \to x \neq y)$
16	11 12 15	3bitri	$⊢ (x = y \to \neg x \in B) \leftrightarrow (y \in B \to x \neq y)$
17	8 16	bitri	$⊢ (y = x \to \neg x \in B) \leftrightarrow (y \in B \to x \neq y)$
18	17	albii	$⊢ \forall y (y = x \to \neg x \in B) \leftrightarrow \forall y (y \in B \to x \neq y)$
19	5 6 18	3bitri	$⊢ \neg x \in B \leftrightarrow \forall y (y \in B \to x \neq y)$
20		df-ral	$⊢ \forall y \in B x \neq y \leftrightarrow \forall y (y \in B \to x \neq y)$
21	19 20	bitr4i	$⊢ \neg x \in B \leftrightarrow \forall y \in B x \neq y$
22	21	rabbii	$⊢ \{x \in A \| \neg x \in B\} = \{x \in A \| \forall y \in B x \neq y\}$
23	1 22	eqtri	$⊢ A ∖ B = \{x \in A \| \forall y \in B x \neq y\}$

Metamath Proof Explorer

Theorem dfdif3

Proof