difab

Description: Difference of two class abstractions. (Contributed by NM, 23-Oct-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Step	Hyp	Ref	Expression
1		df-clab	$⊢ y \in \{x \| (φ \land \neg ψ)\} \leftrightarrow [y/ x] (φ \land \neg ψ)$
2		sban	$⊢ [y/ x] (φ \land \neg ψ) \leftrightarrow ([y/ x] φ \land [y/ x] \neg ψ)$
3		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
4	3	bicomi	$⊢ [y/ x] φ \leftrightarrow y \in \{x \| φ\}$
5		sbn	$⊢ [y/ x] \neg ψ \leftrightarrow \neg [y/ x] ψ$
6		df-clab	$⊢ y \in \{x \| ψ\} \leftrightarrow [y/ x] ψ$
7	5 6	xchbinxr	$⊢ [y/ x] \neg ψ \leftrightarrow \neg y \in \{x \| ψ\}$
8	4 7	anbi12i	$⊢ ([y/ x] φ \land [y/ x] \neg ψ) \leftrightarrow (y \in \{x \| φ\} \land \neg y \in \{x \| ψ\})$
9	1 2 8	3bitrri	$⊢ (y \in \{x \| φ\} \land \neg y \in \{x \| ψ\}) \leftrightarrow y \in \{x \| (φ \land \neg ψ)\}$
10	9	difeqri	$⊢ \{x \| φ\} ∖ \{x \| ψ\} = \{x \| (φ \land \neg ψ)\}$

Metamath Proof Explorer