Theorem ssdif0 4297

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 402	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3897	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4277	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539   ∈ wcel 2106   ∖ cdif 3884   ⊆ wss 3887  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  difn0  4298  pssdifn0  4299  difidALT  4305  vdif0  4402  difrab0eq  4403  difin0  4407  symdifv  5015  frpoind  6245  wfiOLD  6254  ordintdif  6315  dffv2  6863  fndifnfp  7048  tfi  7700  peano5  7740  peano5OLD  7741  frrlem13  8114  frrlem14  8115  wfrlem8OLD  8147  wfrlem16OLD  8155  tz7.49  8276  oe0m1  8351  sucdom2OLD  8869  sdomdif  8912  sucdom2  8989  php3  8995  php3OLD  9007  isinf  9036  unxpwdom2  9347  frind  9508  fin23lem26  10081  fin23lem21  10095  fin1a2lem13  10168  zornn0g  10261  fpwwe2lem12  10398  fpwwe2  10399  isumltss  15560  rpnnen2lem12  15934  symgsssg  19075  symgfisg  19076  psgnunilem5  19102  lspsnat  20407  lsppratlem6  20414  lspprat  20415  lbsextlem4  20423  cnsubrg  20658  opsrtoslem2  21263  0ntr  22222  cmpfi  22559  dfconn2  22570  filconn  23034  cfinfil  23044  ufileu  23070  alexsublem  23195  ptcmplem2  23204  ptcmplem3  23205  restmetu  23726  reconnlem1  23989  bcthlem5  24492  itg10  24852  limcnlp  25042  upgrex  27462  uvtx01vtx  27764  ex-dif  28787  strlem1  30612  difininv  30864  eqdif  30866  difioo  31103  pmtrcnelor  31360  baselcarsg  32273  difelcarsg  32277  sibfof  32307  sitg0  32313  chtvalz  32609  noextendseq  33870  sltlpss  34087  onsucconni  34626  topdifinfeq  35521  nlpineqsn  35579  fdc  35903  setindtr  40846  relnonrel  41195  inaex  41915  caragenunidm  44046