# 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 ${⊢}{A}\cap {B}\subseteq {C}↔{A}\cap \left({B}\setminus {C}\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
2 1 imbi1i ${⊢}\left({x}\in \left({A}\cap {B}\right)\to {x}\in {C}\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\to {x}\in {C}\right)$
3 iman ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\to {x}\in {C}\right)↔¬\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge ¬{x}\in {C}\right)$
4 2 3 bitri ${⊢}\left({x}\in \left({A}\cap {B}\right)\to {x}\in {C}\right)↔¬\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge ¬{x}\in {C}\right)$
5 eldif ${⊢}{x}\in \left({B}\setminus {C}\right)↔\left({x}\in {B}\wedge ¬{x}\in {C}\right)$
6 5 anbi2i ${⊢}\left({x}\in {A}\wedge {x}\in \left({B}\setminus {C}\right)\right)↔\left({x}\in {A}\wedge \left({x}\in {B}\wedge ¬{x}\in {C}\right)\right)$
7 elin ${⊢}{x}\in \left({A}\cap \left({B}\setminus {C}\right)\right)↔\left({x}\in {A}\wedge {x}\in \left({B}\setminus {C}\right)\right)$
8 anass ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge ¬{x}\in {C}\right)↔\left({x}\in {A}\wedge \left({x}\in {B}\wedge ¬{x}\in {C}\right)\right)$
9 6 7 8 3bitr4ri ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)\wedge ¬{x}\in {C}\right)↔{x}\in \left({A}\cap \left({B}\setminus {C}\right)\right)$
10 4 9 xchbinx ${⊢}\left({x}\in \left({A}\cap {B}\right)\to {x}\in {C}\right)↔¬{x}\in \left({A}\cap \left({B}\setminus {C}\right)\right)$
11 10 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cap {B}\right)\to {x}\in {C}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({A}\cap \left({B}\setminus {C}\right)\right)$
12 dfss2 ${⊢}{A}\cap {B}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cap {B}\right)\to {x}\in {C}\right)$
13 eq0 ${⊢}{A}\cap \left({B}\setminus {C}\right)=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({A}\cap \left({B}\setminus {C}\right)\right)$
14 11 12 13 3bitr4i ${⊢}{A}\cap {B}\subseteq {C}↔{A}\cap \left({B}\setminus {C}\right)=\varnothing$