Theorem ssdif0 4319

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 405	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3914	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 337	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1839	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3921	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4302	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1558   = wceq 1560   ∈ wcel 2142   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921  df-nul 4286

This theorem is referenced by:  difn0  4320  pssdifn0  4321  difidALT  4330  vdif0  4423  difrab0eq  4424  difin0  4428  symdifv  5043  frpoind  6329  ordintdif  6397  dffv2  6962  fndifnfp  7160  tfi  7833  peano5  7874  frrlem13  8279  frrlem14  8280  tz7.49  8416  oe0m1  8490  sdomdif  9097  sucdom2  9171  php3  9177  isinf  9209  unxpwdom2  9536  frind  9708  fin23lem26  10282  fin23lem21  10296  fin1a2lem13  10369  zornn0g  10462  fpwwe2lem12  10600  fpwwe2  10601  isumltss  15878  rpnnen2lem12  16257  chnccat  18658  symgsssg  19507  symgfisg  19508  psgnunilem5  19534  lspsnat  21212  lsppratlem6  21219  lspprat  21220  lbsextlem4  21228  cnsubrg  21476  opsrtoslem2  22106  psdmullem  22227  0ntr  23128  cmpfi  23465  dfconn2  23476  filconn  23940  cfinfil  23950  ufileu  23976  alexsublem  24101  ptcmplem2  24110  ptcmplem3  24111  restmetu  24627  reconnlem1  24884  bcthlem5  25387  itg10  25747  limcnlp  25937  noextendseq  27728  ltslpss  27998  upgrex  29290  uvtx01vtx  29595  ex-dif  30622  strlem1  32450  difininv  32713  eqdif  32715  difioo  32981  pmtrcnelor  33268  dflringlem3  33689  dflring4  33691  baselcarsg  34600  difelcarsg  34604  sibfof  34634  sitg0  34640  chtvalz  34920  onvf1odlem2  35444  onsucconni  36794  ttcwf2  36882  topdifinfeq  37841  nlpineqsn  37899  fdc  38241  setindtr  43598  oe0rif  43859  cantnfresb  43898  relnonrel  44160  inaex  44870  caragenunidm  47079