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

Theorem ssdif0 4252
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 3853 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 338 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1826 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3863 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 4232 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 306 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1540   = wceq 1542  wcel 2114  cdif 3840  wss 3843  c0 4211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-in 3850  df-ss 3860  df-nul 4212
This theorem is referenced by:  difn0  4253  pssdifn0  4254  difidALT  4260  vdif0  4358  difrab0eq  4359  difin0  4363  symdifv  4971  wfi  6162  ordintdif  6221  dffv2  6765  fndifnfp  6950  tfi  7589  peano5  7626  peano5OLD  7627  wfrlem8  7993  wfrlem16  8001  tz7.49  8112  oe0m1  8179  sucdom2  8678  sdomdif  8717  php3  8755  isinf  8812  unxpwdom2  9127  fin23lem26  9827  fin23lem21  9841  fin1a2lem13  9914  zornn0g  10007  fpwwe2lem12  10144  fpwwe2  10145  isumltss  15298  rpnnen2lem12  15672  symgsssg  18715  symgfisg  18716  psgnunilem5  18742  lspsnat  20038  lsppratlem6  20045  lspprat  20046  lbsextlem4  20054  cnsubrg  20279  opsrtoslem2  20869  0ntr  21824  cmpfi  22161  dfconn2  22172  filconn  22636  cfinfil  22646  ufileu  22672  alexsublem  22797  ptcmplem2  22806  ptcmplem3  22807  restmetu  23325  reconnlem1  23580  bcthlem5  24082  itg10  24442  limcnlp  24632  upgrex  27039  uvtx01vtx  27341  ex-dif  28362  strlem1  30187  difininv  30440  eqdif  30442  difioo  30680  pmtrcnelor  30939  baselcarsg  31845  difelcarsg  31849  sibfof  31879  sitg0  31885  chtvalz  32181  frpoind  33387  frind  33395  frrlem13  33457  frrlem14  33458  noextendseq  33515  sltlpss  33732  onsucconni  34271  topdifinfeq  35166  nlpineqsn  35224  fdc  35548  setindtr  40440  relnonrel  40762  inaex  41479  caragenunidm  43610
  Copyright terms: Public domain W3C validator