Theorem ssdif0 4371

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

Assertion

Ref	Expression
ssdif0	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Proof of Theorem ssdif0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iman 401	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3972	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1815	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3979	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4355	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536   ∈ wcel 2105   ∖ cdif 3959   ⊆ wss 3962  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979  df-nul 4339

This theorem is referenced by:  difn0  4372  pssdifn0  4373  difidALT  4382  vdif0  4474  difrab0eq  4475  difin0  4479  symdifv  5090  frpoind  6364  wfiOLD  6373  ordintdif  6435  dffv2  7003  fndifnfp  7195  tfi  7873  peano5  7915  frrlem13  8321  frrlem14  8322  wfrlem8OLD  8354  wfrlem16OLD  8362  tz7.49  8483  oe0m1  8557  sucdom2OLD  9120  sdomdif  9163  sucdom2  9240  php3  9246  php3OLD  9258  isinf  9293  isinfOLD  9294  unxpwdom2  9625  frind  9787  fin23lem26  10362  fin23lem21  10376  fin1a2lem13  10449  zornn0g  10542  fpwwe2lem12  10679  fpwwe2  10680  isumltss  15880  rpnnen2lem12  16257  symgsssg  19499  symgfisg  19500  psgnunilem5  19526  lspsnat  21164  lsppratlem6  21171  lspprat  21172  lbsextlem4  21180  cnsubrg  21462  opsrtoslem2  22097  psdmullem  22186  0ntr  23094  cmpfi  23431  dfconn2  23442  filconn  23906  cfinfil  23916  ufileu  23942  alexsublem  24067  ptcmplem2  24076  ptcmplem3  24077  restmetu  24598  reconnlem1  24861  bcthlem5  25375  itg10  25736  limcnlp  25927  noextendseq  27726  sltlpss  27959  upgrex  29123  uvtx01vtx  29428  ex-dif  30451  strlem1  32278  difininv  32544  eqdif  32546  difioo  32790  pmtrcnelor  33093  baselcarsg  34287  difelcarsg  34291  sibfof  34321  sitg0  34327  chtvalz  34622  onsucconni  36419  topdifinfeq  37332  nlpineqsn  37390  fdc  37731  setindtr  43012  oe0rif  43274  cantnfresb  43313  relnonrel  43576  inaex  44292  caragenunidm  46463