Theorem 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	$$⊢\left\{x|\phi \right\}\setminus \left\{x|\psi \right\}=\left\{x|\left(\phi \wedge \neg \psi \right)\right\}$$

Proof

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