eldif

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994)

		Ref	Expression
	Assertion	eldif	$⊢ A \in (B ∖ C) \leftrightarrow (A \in B \land \neg A \in C)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in (B ∖ C) \to A \in V$
2		elex	$⊢ A \in B \to A \in V$
3	2	adantr	$⊢ (A \in B \land \neg A \in C) \to A \in V$
4		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
5		eleq1	$⊢ x = A \to (x \in C \leftrightarrow A \in C)$
6	5	notbid	$⊢ x = A \to (\neg x \in C \leftrightarrow \neg A \in C)$
7	4 6	anbi12d	$⊢ x = A \to ((x \in B \land \neg x \in C) \leftrightarrow (A \in B \land \neg A \in C))$
8		df-dif	$⊢ B ∖ C = \{x \| (x \in B \land \neg x \in C)\}$
9	7 8	elab2g	$⊢ A \in V \to (A \in (B ∖ C) \leftrightarrow (A \in B \land \neg A \in C))$
10	1 3 9	pm5.21nii	$⊢ A \in (B ∖ C) \leftrightarrow (A \in B \land \neg A \in C)$

Metamath Proof Explorer