Theorem ssdif0 3975

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 439	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3617	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 324	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1787	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3624	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 3962	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523   ∈ wcel 2030   ∖ cdif 3604   ⊆ wss 3607  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949

This theorem is referenced by:  difn0  3976  pssdifn0  3977  difid  3981  vdif0  4070  difrab0eq  4071  difin0  4074  symdifv  4630  wfi  5751  ordintdif  5812  dffv2  6310  fndifnfp  6483  tfi  7095  peano5  7131  wfrlem8  7467  wfrlem16  7475  tz7.49  7585  oe0m1  7646  sdomdif  8149  php3  8187  sucdom2  8197  isinf  8214  unxpwdom2  8534  fin23lem26  9185  fin23lem21  9199  fin1a2lem13  9272  zornn0g  9365  fpwwe2lem13  9502  fpwwe2  9503  isumltss  14624  rpnnen2lem12  14998  symgsssg  17933  symgfisg  17934  psgnunilem5  17960  lspsnat  19193  lsppratlem6  19200  lspprat  19201  lbsextlem4  19209  opsrtoslem2  19533  cnsubrg  19854  0ntr  20923  cmpfi  21259  dfconn2  21270  filconn  21734  cfinfil  21744  ufileu  21770  alexsublem  21895  ptcmplem2  21904  ptcmplem3  21905  restmetu  22422  reconnlem1  22676  bcthlem5  23171  itg10  23500  limcnlp  23687  upgrex  26032  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  ex-dif  27410  strlem1  29237  difininv  29480  difioo  29672  baselcarsg  30496  difelcarsg  30500  sibfof  30530  sitg0  30536  chtvalz  30835  frpoind  31865  frind  31868  noextendseq  31945  onsucconni  32561  topdifinfeq  33328  fdc  33671  setindtr  37908  relnonrel  38210  caragenunidm  41043