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

Theorem ssdif0 4296
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 405 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 eldif 3920 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 338 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1821 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3930 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 4281 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 306 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2115  cdif 3907  wss 3910  c0 4266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473  df-dif 3913  df-in 3917  df-ss 3927  df-nul 4267
This theorem is referenced by:  difn0  4297  pssdifn0  4298  difid  4303  vdif0  4391  difrab0eq  4392  difin0  4395  symdifv  4981  wfi  6154  ordintdif  6213  dffv2  6729  fndifnfp  6911  tfi  7543  peano5  7580  wfrlem8  7937  wfrlem16  7945  tz7.49  8056  oe0m1  8121  sucdom2  8602  sdomdif  8641  php3  8679  isinf  8707  unxpwdom2  9028  fin23lem26  9724  fin23lem21  9738  fin1a2lem13  9811  zornn0g  9904  fpwwe2lem13  10041  fpwwe2  10042  isumltss  15182  rpnnen2lem12  15557  symgsssg  18574  symgfisg  18575  psgnunilem5  18601  lspsnat  19893  lsppratlem6  19900  lspprat  19901  lbsextlem4  19909  opsrtoslem2  20241  cnsubrg  20581  0ntr  21655  cmpfi  21992  dfconn2  22003  filconn  22467  cfinfil  22477  ufileu  22503  alexsublem  22628  ptcmplem2  22637  ptcmplem3  22638  restmetu  23156  reconnlem1  23410  bcthlem5  23911  itg10  24271  limcnlp  24460  upgrex  26864  uvtx01vtx  27166  ex-dif  28187  strlem1  30012  difininv  30266  eqdif  30268  difioo  30492  pmtrcnelor  30743  baselcarsg  31572  difelcarsg  31576  sibfof  31606  sitg0  31612  chtvalz  31908  frpoind  33088  frind  33093  frrlem13  33143  frrlem14  33144  noextendseq  33182  onsucconni  33793  topdifinfeq  34655  nlpineqsn  34713  fdc  35069  setindtr  39776  relnonrel  40098  inaex  40820  caragenunidm  42970
  Copyright terms: Public domain W3C validator