Theorem ssdif0 4332

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 401	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3927	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3934	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4316	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ∖ cdif 3914   ⊆ wss 3917  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934  df-nul 4300

This theorem is referenced by:  difn0  4333  pssdifn0  4334  difidALT  4343  vdif0  4435  difrab0eq  4436  difin0  4440  symdifv  5053  frpoind  6318  ordintdif  6386  dffv2  6959  fndifnfp  7153  tfi  7832  peano5  7872  frrlem13  8280  frrlem14  8281  tz7.49  8416  oe0m1  8488  sucdom2OLD  9056  sdomdif  9095  sucdom2  9173  php3  9179  isinf  9214  isinfOLD  9215  unxpwdom2  9548  frind  9710  fin23lem26  10285  fin23lem21  10299  fin1a2lem13  10372  zornn0g  10465  fpwwe2lem12  10602  fpwwe2  10603  isumltss  15821  rpnnen2lem12  16200  symgsssg  19404  symgfisg  19405  psgnunilem5  19431  lspsnat  21062  lsppratlem6  21069  lspprat  21070  lbsextlem4  21078  cnsubrg  21351  opsrtoslem2  21970  psdmullem  22059  0ntr  22965  cmpfi  23302  dfconn2  23313  filconn  23777  cfinfil  23787  ufileu  23813  alexsublem  23938  ptcmplem2  23947  ptcmplem3  23948  restmetu  24465  reconnlem1  24722  bcthlem5  25235  itg10  25596  limcnlp  25786  noextendseq  27586  sltlpss  27826  upgrex  29026  uvtx01vtx  29331  ex-dif  30359  strlem1  32186  difininv  32453  eqdif  32455  difioo  32712  pmtrcnelor  33055  baselcarsg  34304  difelcarsg  34308  sibfof  34338  sitg0  34344  chtvalz  34627  onvf1odlem2  35098  onsucconni  36432  topdifinfeq  37345  nlpineqsn  37403  fdc  37746  setindtr  43020  oe0rif  43281  cantnfresb  43320  relnonrel  43583  inaex  44293  caragenunidm  46513