Theorem ssdif0 4317

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 3913	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4301	. 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 3900   ⊆ wss 3903  ∅c0 4284

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920  df-nul 4285

This theorem is referenced by:  difn0  4318  pssdifn0  4319  difidALT  4328  vdif0  4420  difrab0eq  4421  difin0  4425  symdifv  5035  frpoind  6290  ordintdif  6358  dffv2  6918  fndifnfp  7112  tfi  7786  peano5  7826  frrlem13  8231  frrlem14  8232  tz7.49  8367  oe0m1  8439  sdomdif  9042  sucdom2  9117  php3  9123  isinf  9154  unxpwdom2  9480  frind  9646  fin23lem26  10219  fin23lem21  10233  fin1a2lem13  10306  zornn0g  10399  fpwwe2lem12  10536  fpwwe2  10537  isumltss  15755  rpnnen2lem12  16134  symgsssg  19346  symgfisg  19347  psgnunilem5  19373  lspsnat  21052  lsppratlem6  21059  lspprat  21060  lbsextlem4  21068  cnsubrg  21334  opsrtoslem2  21961  psdmullem  22050  0ntr  22956  cmpfi  23293  dfconn2  23304  filconn  23768  cfinfil  23778  ufileu  23804  alexsublem  23929  ptcmplem2  23938  ptcmplem3  23939  restmetu  24456  reconnlem1  24713  bcthlem5  25226  itg10  25587  limcnlp  25777  noextendseq  27577  sltlpss  27822  upgrex  29037  uvtx01vtx  29342  ex-dif  30367  strlem1  32194  difininv  32461  eqdif  32463  difioo  32725  pmtrcnelor  33033  baselcarsg  34274  difelcarsg  34278  sibfof  34308  sitg0  34314  chtvalz  34597  onvf1odlem2  35077  onsucconni  36411  topdifinfeq  37324  nlpineqsn  37382  fdc  37725  setindtr  42997  oe0rif  43258  cantnfresb  43297  relnonrel  43560  inaex  44270  caragenunidm  46489