Theorem ssdif0 4314

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 3909	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4297	. 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 2145   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  difn0  4315  pssdifn0  4316  inssdif0  4322  difidALT  4326  vdif0  4422  difrab0eq  4423  difin0  4428  symdifv  5046  frpoind  6344  ordintdif  6413  dffv2  6978  fndifnfp  7179  tfi  7862  peano5  7903  frrlem13  8309  frrlem14  8310  tz7.49  8448  oe0m1  8522  sdomdif  9137  sucdom2  9211  php3  9217  isinf  9249  unxpwdom2  9575  frind  9747  fin23lem26  10396  fin23lem21  10410  fin1a2lem13  10483  zornn0g  10576  fpwwe2lem12  10720  fpwwe2  10721  isumltss  16010  rpnnen2lem12  16386  chnccat  18793  symgsssg  19674  symgfisg  19675  psgnunilem5  19701  lspsnat  21416  lsppratlem6  21423  lspprat  21424  lbsextlem4  21432  cnsubrg  21726  opsrtoslem2  22358  psdmullem  22479  0ntr  23382  cmpfi  23719  dfconn2  23730  filconn  24195  cfinfil  24205  ufileu  24231  alexsublem  24356  ptcmplem2  24365  ptcmplem3  24366  restmetu  24882  reconnlem1  25139  bcthlem5  25642  itg10  26002  limcnlp  26191  noextendseq  28017  ltslpss  28287  upgrex  29663  uvtx01vtx  29971  ex-dif  31017  strlem1  32845  difininv  33106  eqdif  33108  difioo  33367  pmtrcnelor  33645  dflringlem3  34021  dflring4  34023  baselcarsg  34931  difelcarsg  34935  sibfof  34965  sitg0  34971  chtvalz  35251  onvf1odlem2  35866  onsucconni  37205  ttcwf2  37293  topdifinfeq  38253  nlpineqsn  38311  fdc  38659  setindtr  44010  oe0rif  44271  cantnfresb  44310  relnonrel  44572  inaex  45266  caragenunidm  47487