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	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
Assertion	difeqri	⊢ ( 𝐴 ∖ 𝐵 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		difeqri.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
2		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
3	2 1	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ 𝑥 ∈ 𝐶 )
4	3	eqriv	⊢ ( 𝐴 ∖ 𝐵 ) = 𝐶