Metamath Proof Explorer

Theorem ssdif0

Description: Subclass expressed in terms of difference. Exercise 7 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion ssdif0 ${⊢}{A}\subseteq {B}↔{A}\setminus {B}=\varnothing$

Proof

Step Hyp Ref Expression
1 iman ${⊢}\left({x}\in {A}\to {x}\in {B}\right)↔¬\left({x}\in {A}\wedge ¬{x}\in {B}\right)$
2 eldif ${⊢}{x}\in \left({A}\setminus {B}\right)↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)$
3 1 2 xchbinxr ${⊢}\left({x}\in {A}\to {x}\in {B}\right)↔¬{x}\in \left({A}\setminus {B}\right)$
4 3 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({A}\setminus {B}\right)$
5 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
6 eq0 ${⊢}{A}\setminus {B}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({A}\setminus {B}\right)$
7 4 5 6 3bitr4i ${⊢}{A}\subseteq {B}↔{A}\setminus {B}=\varnothing$