Theorem ssdif0 4329

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567   ∈ wcel 2149   ∖ cdif 3910   ⊆ wss 3913  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930  df-nul 4295

This theorem is referenced by:  difn0  4330  pssdifn0  4331  difidALT  4340  vdif0  4435  difrab0eq  4436  difin0  4440  symdifv  5056  frpoind  6344  ordintdif  6413  dffv2  6977  fndifnfp  7175  tfi  7848  peano5  7889  frrlem13  8294  frrlem14  8295  tz7.49  8431  oe0m1  8505  sdomdif  9112  sucdom2  9186  php3  9192  isinf  9224  unxpwdom2  9549  frind  9721  fin23lem26  10308  fin23lem21  10322  fin1a2lem13  10395  zornn0g  10488  fpwwe2lem12  10626  fpwwe2  10627  isumltss  15901  rpnnen2lem12  16280  chnccat  18681  symgsssg  19536  symgfisg  19537  psgnunilem5  19563  lspsnat  21246  lsppratlem6  21253  lspprat  21254  lbsextlem4  21262  cnsubrg  21545  opsrtoslem2  22175  psdmullem  22296  0ntr  23196  cmpfi  23533  dfconn2  23544  filconn  24008  cfinfil  24018  ufileu  24044  alexsublem  24169  ptcmplem2  24178  ptcmplem3  24179  restmetu  24695  reconnlem1  24952  bcthlem5  25455  itg10  25815  limcnlp  26005  noextendseq  27796  ltslpss  28066  upgrex  29382  uvtx01vtx  29687  ex-dif  30714  strlem1  32542  difininv  32803  eqdif  32805  difioo  33067  pmtrcnelor  33351  dflringlem3  33730  dflring4  33732  baselcarsg  34640  difelcarsg  34644  sibfof  34674  sitg0  34680  chtvalz  34960  onvf1odlem2  35486  onsucconni  36836  ttcwf2  36924  topdifinfeq  37883  nlpineqsn  37941  fdc  38283  setindtr  43642  oe0rif  43903  cantnfresb  43942  relnonrel  44204  inaex  44898  caragenunidm  47113