Theorem ssdif0 4313

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569   ∈ wcel 2144   ⊆ wss 3896   ∖ cdif 4044  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-dif 4046  df-nul 4278

This theorem is used by:  difn0  4314  pssdifn0  4315  inssdif0  4321  difidALT  4325  vdif0  4421  difrab0eq  4422  difin0  4427  symdifv  5045  frpoind  6348  ordintdif  6417  dffv2  6985  fndifnfp  7185  tfi  7868  peano5  7909  frrlem13  8323  frrlem14  8324  tz7.49  8462  oe0m1  8536  sdomdif  9151  sucdom2  9225  php3  9231  isinf  9263  unxpwdom2  9589  frind  9761  fin23lem26  10410  fin23lem21  10424  fin1a2lem13  10497  zornn0g  10590  fpwwe2lem12  10734  fpwwe2  10735  isumltss  16026  rpnnen2lem12  16402  chnccat  18809  symgsssg  19690  symgfisg  19691  psgnunilem5  19717  lspsnat  21432  lsppratlem6  21439  lspprat  21440  lbsextlem4  21448  cnsubrg  21742  opsrtoslem2  22374  psdmullem  22495  0ntr  23398  cmpfi  23735  dfconn2  23746  filconn  24211  cfinfil  24221  ufileu  24247  alexsublem  24372  ptcmplem2  24381  ptcmplem3  24382  restmetu  24898  reconnlem1  25155  bcthlem5  25658  itg10  26018  limcnlp  26207  noextendseq  28033  ltslpss  28303  upgrex  29679  uvtx01vtx  29987  ex-dif  31033  strlem1  32861  difininv  33164  eqdif  33166  difioo  33424  pmtrcnelor  33702  dflringlem3  34078  dflring4  34080  baselcarsg  34988  difelcarsg  34992  sibfof  35022  sitg0  35028  chtvalz  35308  onvf1odlem2  35955  onsucconni  37321  ttcwf2  37409  topdifinfeq  38382  nlpineqsn  38440  fdc  38788  setindtr  44140  oe0rif  44396  cantnfresb  44435  relnonrel  44696  inaex  45390  caragenunidm  47626