Theorem ssdif0 4321

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 407	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3916	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3923	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4304	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2146   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923  df-nul 4287

This theorem is used by:  difn0  4322  pssdifn0  4323  inssdif0  4329  difidALT  4333  vdif0  4429  difrab0eq  4430  difin0  4435  symdifv  5054  frpoind  6347  ordintdif  6416  dffv2  6980  fndifnfp  7180  tfi  7855  peano5  7896  frrlem13  8301  frrlem14  8302  tz7.49  8438  oe0m1  8512  sdomdif  9120  sucdom2  9194  php3  9200  isinf  9232  unxpwdom2  9557  frind  9729  fin23lem26  10324  fin23lem21  10338  fin1a2lem13  10411  zornn0g  10504  fpwwe2lem12  10642  fpwwe2  10643  isumltss  15925  rpnnen2lem12  16303  chnccat  18704  symgsssg  19581  symgfisg  19582  psgnunilem5  19608  lspsnat  21319  lsppratlem6  21326  lspprat  21327  lbsextlem4  21335  cnsubrg  21627  opsrtoslem2  22257  psdmullem  22378  0ntr  23278  cmpfi  23615  dfconn2  23626  filconn  24091  cfinfil  24101  ufileu  24127  alexsublem  24252  ptcmplem2  24261  ptcmplem3  24262  restmetu  24778  reconnlem1  25035  bcthlem5  25538  itg10  25898  limcnlp  26088  noextendseq  27882  ltslpss  28152  upgrex  29497  uvtx01vtx  29805  ex-dif  30845  strlem1  32673  difininv  32934  eqdif  32936  difioo  33197  pmtrcnelor  33475  dflringlem3  33850  dflring4  33852  baselcarsg  34761  difelcarsg  34765  sibfof  34795  sitg0  34801  chtvalz  35081  onvf1odlem2  35645  onsucconni  37005  ttcwf2  37093  topdifinfeq  38053  nlpineqsn  38111  fdc  38454  setindtr  43809  oe0rif  44070  cantnfresb  44109  relnonrel  44371  inaex  45065  caragenunidm  47280