# Metamath Proof Explorer

## 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)

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

### Proof

Step Hyp Ref Expression
1 elin ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
2 1 imbi1i ( ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐶 ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) → 𝑥𝐶 ) )
3 iman ( ( ( 𝑥𝐴𝑥𝐵 ) → 𝑥𝐶 ) ↔ ¬ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ¬ 𝑥𝐶 ) )
4 2 3 bitri ( ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐶 ) ↔ ¬ ( ( 𝑥𝐴𝑥𝐵 ) ∧ ¬ 𝑥𝐶 ) )
5 eldif ( 𝑥 ∈ ( 𝐵𝐶 ) ↔ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) )
6 5 anbi2i ( ( 𝑥𝐴𝑥 ∈ ( 𝐵𝐶 ) ) ↔ ( 𝑥𝐴 ∧ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) ) )
7 elin ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵𝐶 ) ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐵𝐶 ) ) )
8 anass ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ¬ 𝑥𝐶 ) ↔ ( 𝑥𝐴 ∧ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶 ) ) )
9 6 7 8 3bitr4ri ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ ¬ 𝑥𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
10 4 9 xchbinx ( ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐶 ) ↔ ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
11 10 albii ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐶 ) ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
12 dfss2 ( ( 𝐴𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴𝐵 ) → 𝑥𝐶 ) )
13 eq0 ( ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵𝐶 ) ) )
14 11 12 13 3bitr4i ( ( 𝐴𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ∅ )