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

Metamath Proof Explorer

Theorem dfin2

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 . Another version is given by dfin4 . (Contributed by NM, 10-Jun-2004)

		Ref	Expression
	Assertion	dfin2	$⊢ A \cap B = A ∖ (V ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		velcomp	$⊢ x \in (V ∖ B) \leftrightarrow \neg x \in B$
2	1	con2bii	$⊢ x \in B \leftrightarrow \neg x \in (V ∖ B)$
3	2	anbi2i	$⊢ (x \in A \land x \in B) \leftrightarrow (x \in A \land \neg x \in (V ∖ B))$
4		eldif	$⊢ x \in (A ∖ (V ∖ B)) \leftrightarrow (x \in A \land \neg x \in (V ∖ B))$
5	3 4	bitr4i	$⊢ (x \in A \land x \in B) \leftrightarrow x \in (A ∖ (V ∖ B))$
6	5	ineqri	$⊢ A \cap B = A ∖ (V ∖ B)$