Theorem ssdif0 4364

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 403	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3959	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3969	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4344	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ∖ cdif 3946   ⊆ wss 3949  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  difn0  4365  pssdifn0  4366  difidALT  4372  vdif0  4469  difrab0eq  4470  difin0  4474  symdifv  5090  frpoind  6344  wfiOLD  6353  ordintdif  6415  dffv2  6987  fndifnfp  7174  tfi  7842  peano5  7884  peano5OLD  7885  frrlem13  8283  frrlem14  8284  wfrlem8OLD  8316  wfrlem16OLD  8324  tz7.49  8445  oe0m1  8521  sucdom2OLD  9082  sdomdif  9125  sucdom2  9206  php3  9212  php3OLD  9224  isinf  9260  isinfOLD  9261  unxpwdom2  9583  frind  9745  fin23lem26  10320  fin23lem21  10334  fin1a2lem13  10407  zornn0g  10500  fpwwe2lem12  10637  fpwwe2  10638  isumltss  15794  rpnnen2lem12  16168  symgsssg  19335  symgfisg  19336  psgnunilem5  19362  lspsnat  20758  lsppratlem6  20765  lspprat  20766  lbsextlem4  20774  cnsubrg  21005  opsrtoslem2  21617  0ntr  22575  cmpfi  22912  dfconn2  22923  filconn  23387  cfinfil  23397  ufileu  23423  alexsublem  23548  ptcmplem2  23557  ptcmplem3  23558  restmetu  24079  reconnlem1  24342  bcthlem5  24845  itg10  25205  limcnlp  25395  noextendseq  27170  sltlpss  27402  upgrex  28383  uvtx01vtx  28685  ex-dif  29707  strlem1  31534  difininv  31786  eqdif  31788  difioo  32024  pmtrcnelor  32283  baselcarsg  33336  difelcarsg  33340  sibfof  33370  sitg0  33376  chtvalz  33672  onsucconni  35370  topdifinfeq  36279  nlpineqsn  36337  fdc  36661  setindtr  41811  oe0rif  42083  cantnfresb  42122  relnonrel  42386  inaex  43104  caragenunidm  45272