Theorem ssdif0 4294

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 3893	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 336	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3900	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4278	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 304	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-ss 3900  df-nul 4262

This theorem is referenced by:  difn0  4295  pssdifn0  4296  difidALT  4305  vdif0  4397  difrab0eq  4398  difin0  4402  symdifv  5015  frpoind  6293  ordintdif  6361  dffv2  6922  fndifnfp  7120  tfi  7793  peano5  7833  frrlem13  8238  frrlem14  8239  tz7.49  8374  oe0m1  8446  sdomdif  9053  sucdom2  9127  php3  9133  isinf  9165  unxpwdom2  9493  frind  9665  fin23lem26  10238  fin23lem21  10252  fin1a2lem13  10325  zornn0g  10418  fpwwe2lem12  10556  fpwwe2  10557  isumltss  15804  rpnnen2lem12  16183  chnccat  18583  symgsssg  19433  symgfisg  19434  psgnunilem5  19460  lspsnat  21138  lsppratlem6  21145  lspprat  21146  lbsextlem4  21154  cnsubrg  21402  opsrtoslem2  22032  psdmullem  22153  0ntr  23054  cmpfi  23391  dfconn2  23402  filconn  23866  cfinfil  23876  ufileu  23902  alexsublem  24027  ptcmplem2  24036  ptcmplem3  24037  restmetu  24553  reconnlem1  24810  bcthlem5  25313  itg10  25673  limcnlp  25863  noextendseq  27649  ltslpss  27918  upgrex  29179  uvtx01vtx  29484  ex-dif  30511  strlem1  32339  difininv  32605  eqdif  32607  difioo  32874  pmtrcnelor  33172  baselcarsg  34490  difelcarsg  34494  sibfof  34524  sitg0  34530  chtvalz  34813  onvf1odlem2  35332  onsucconni  36665  ttcwf2  36753  topdifinfeq  37712  nlpineqsn  37770  fdc  38112  setindtr  43469  oe0rif  43730  cantnfresb  43769  relnonrel  44031  inaex  44741  caragenunidm  46951