Metamath Proof Explorer

Theorem difrab

Description: Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004)

		Ref	Expression
	Assertion	difrab	$⊢ \{x \in A \| φ\} ∖ \{x \in A \| ψ\} = \{x \in A \| (φ \land \neg ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
3	1 2	difeq12i	$⊢ \{x \in A \| φ\} ∖ \{x \in A \| ψ\} = \{x \| (x \in A \land φ)\} ∖ \{x \| (x \in A \land ψ)\}$
4		df-rab	$⊢ \{x \in A \| (φ \land \neg ψ)\} = \{x \| (x \in A \land (φ \land \neg ψ))\}$
5		difab	$⊢ \{x \| (x \in A \land φ)\} ∖ \{x \| (x \in A \land ψ)\} = \{x \| ((x \in A \land φ) \land \neg (x \in A \land ψ))\}$
6		anass	$⊢ ((x \in A \land φ) \land \neg ψ) \leftrightarrow (x \in A \land (φ \land \neg ψ))$
7		simpr	$⊢ (x \in A \land ψ) \to ψ$
8	7	con3i	$⊢ \neg ψ \to \neg (x \in A \land ψ)$
9	8	anim2i	$⊢ ((x \in A \land φ) \land \neg ψ) \to ((x \in A \land φ) \land \neg (x \in A \land ψ))$
10		pm3.2	$⊢ x \in A \to (ψ \to (x \in A \land ψ))$
11	10	adantr	$⊢ (x \in A \land φ) \to (ψ \to (x \in A \land ψ))$
12	11	con3d	$⊢ (x \in A \land φ) \to (\neg (x \in A \land ψ) \to \neg ψ)$
13	12	imdistani	$⊢ ((x \in A \land φ) \land \neg (x \in A \land ψ)) \to ((x \in A \land φ) \land \neg ψ)$
14	9 13	impbii	$⊢ ((x \in A \land φ) \land \neg ψ) \leftrightarrow ((x \in A \land φ) \land \neg (x \in A \land ψ))$
15	6 14	bitr3i	$⊢ (x \in A \land (φ \land \neg ψ)) \leftrightarrow ((x \in A \land φ) \land \neg (x \in A \land ψ))$
16	15	abbii	$⊢ \{x \| (x \in A \land (φ \land \neg ψ))\} = \{x \| ((x \in A \land φ) \land \neg (x \in A \land ψ))\}$
17	5 16	eqtr4i	$⊢ \{x \| (x \in A \land φ)\} ∖ \{x \| (x \in A \land ψ)\} = \{x \| (x \in A \land (φ \land \neg ψ))\}$
18	4 17	eqtr4i	$⊢ \{x \in A \| (φ \land \neg ψ)\} = \{x \| (x \in A \land φ)\} ∖ \{x \| (x \in A \land ψ)\}$
19	3 18	eqtr4i	$⊢ \{x \in A \| φ\} ∖ \{x \in A \| ψ\} = \{x \in A \| (φ \land \neg ψ)\}$