MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssdif0 Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 iman 439 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 eldif 3617 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 324 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1787 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3624 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 3962 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 292 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator