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  27401  upgrex  28352  uvtx01vtx  28654  ex-dif  29676  strlem1  31503  difininv  31755  eqdif  31757  difioo  31993  pmtrcnelor  32252  baselcarsg  33305  difelcarsg  33309  sibfof  33339  sitg0  33345  chtvalz  33641  onsucconni  35322  topdifinfeq  36231  nlpineqsn  36289  fdc  36613  setindtr  41763  oe0rif  42035  cantnfresb  42074  relnonrel  42338  inaex  43056  caragenunidm  45224