This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 df-ss ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐶 ) )
13 eq0 ⊢ ( ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) )
14 11 12 13 3bitr4i ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )