This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difjust

Description: Soundness justification theorem for df-dif . (Contributed by Rodolfo Medina, 27-Apr-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

		Ref	Expression
	Assertion	difjust	$⊢ \{x \| (x \in A \land \neg x \in B)\} = \{y \| (y \in A \land \neg y \in B)\}$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
2		eleq1w	$⊢ x = z \to (x \in B \leftrightarrow z \in B)$
3	2	notbid	$⊢ x = z \to (\neg x \in B \leftrightarrow \neg z \in B)$
4	1 3	anbi12d	$⊢ x = z \to ((x \in A \land \neg x \in B) \leftrightarrow (z \in A \land \neg z \in B))$
5	4	cbvabv	$⊢ \{x \| (x \in A \land \neg x \in B)\} = \{z \| (z \in A \land \neg z \in B)\}$
6		eleq1w	$⊢ z = y \to (z \in A \leftrightarrow y \in A)$
7		eleq1w	$⊢ z = y \to (z \in B \leftrightarrow y \in B)$
8	7	notbid	$⊢ z = y \to (\neg z \in B \leftrightarrow \neg y \in B)$
9	6 8	anbi12d	$⊢ z = y \to ((z \in A \land \neg z \in B) \leftrightarrow (y \in A \land \neg y \in B))$
10	9	cbvabv	$⊢ \{z \| (z \in A \land \neg z \in B)\} = \{y \| (y \in A \land \neg y \in B)\}$
11	5 10	eqtri	$⊢ \{x \| (x \in A \land \neg x \in B)\} = \{y \| (y \in A \land \neg y \in B)\}$