Theorem ssdif0 4318

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 3911	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3918	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4302	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ∖ cdif 3898   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918  df-nul 4286

This theorem is referenced by:  difn0  4319  pssdifn0  4320  difidALT  4329  vdif0  4421  difrab0eq  4422  difin0  4426  symdifv  5041  frpoind  6300  ordintdif  6368  dffv2  6929  fndifnfp  7122  tfi  7795  peano5  7835  frrlem13  8240  frrlem14  8241  tz7.49  8376  oe0m1  8448  sdomdif  9053  sucdom2  9127  php3  9133  isinf  9165  unxpwdom2  9493  frind  9662  fin23lem26  10235  fin23lem21  10249  fin1a2lem13  10322  zornn0g  10415  fpwwe2lem12  10553  fpwwe2  10554  isumltss  15771  rpnnen2lem12  16150  chnccat  18549  symgsssg  19396  symgfisg  19397  psgnunilem5  19423  lspsnat  21100  lsppratlem6  21107  lspprat  21108  lbsextlem4  21116  cnsubrg  21382  opsrtoslem2  22011  psdmullem  22108  0ntr  23015  cmpfi  23352  dfconn2  23363  filconn  23827  cfinfil  23837  ufileu  23863  alexsublem  23988  ptcmplem2  23997  ptcmplem3  23998  restmetu  24514  reconnlem1  24771  bcthlem5  25284  itg10  25645  limcnlp  25835  noextendseq  27635  ltslpss  27904  upgrex  29165  uvtx01vtx  29470  ex-dif  30498  strlem1  32325  difininv  32592  eqdif  32594  difioo  32862  pmtrcnelor  33173  baselcarsg  34463  difelcarsg  34467  sibfof  34497  sitg0  34503  chtvalz  34786  onvf1odlem2  35298  onsucconni  36631  topdifinfeq  37555  nlpineqsn  37613  fdc  37946  setindtr  43266  oe0rif  43527  cantnfresb  43566  relnonrel  43828  inaex  44538  caragenunidm  46752