Theorem inssdif0

Description: Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014) (Proof shortened by BJ, 18-Jul-2026)

	Ref	Expression
Assertion	inssdif0	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ssdif0	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ )
2		indif2	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 )
3	2	eqeq1i	⊢ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ∅ )
4	1 3	bitr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )