Theorem difeqri

Description: Inference from membership to difference. (Contributed by NM, 17-May-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Hypothesis	difeqri.1	$$⊢\left(x\in A\wedge \neg x\in B\right)\leftrightarrow x\in C$$
Assertion	difeqri	$$⊢A\setminus B=C$$

Proof

Step	Hyp	Ref	Expression
1		difeqri.1	$$⊢\left(x\in A\wedge \neg x\in B\right)\leftrightarrow x\in C$$
2		eldif	$$⊢x\in \left(A\setminus B\right)\leftrightarrow \left(x\in A\wedge \neg x\in B\right)$$
3	2 1	bitri	$$⊢x\in \left(A\setminus B\right)\leftrightarrow x\in C$$
4	3	eqriv	$$⊢A\setminus B=C$$