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

Theorem ssdif0 4328
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 403 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 eldif 3925 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 335 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1822 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3935 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 4308 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 303 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wcel 2107  cdif 3912  wss 3915  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-in 3922  df-ss 3932  df-nul 4288
This theorem is referenced by:  difn0  4329  pssdifn0  4330  difidALT  4336  vdif0  4433  difrab0eq  4434  difin0  4438  symdifv  5051  frpoind  6301  wfiOLD  6310  ordintdif  6372  dffv2  6941  fndifnfp  7127  tfi  7794  peano5  7835  peano5OLD  7836  frrlem13  8234  frrlem14  8235  wfrlem8OLD  8267  wfrlem16OLD  8275  tz7.49  8396  oe0m1  8472  sucdom2OLD  9033  sdomdif  9076  sucdom2  9157  php3  9163  php3OLD  9175  isinf  9211  isinfOLD  9212  unxpwdom2  9531  frind  9693  fin23lem26  10268  fin23lem21  10282  fin1a2lem13  10355  zornn0g  10448  fpwwe2lem12  10585  fpwwe2  10586  isumltss  15740  rpnnen2lem12  16114  symgsssg  19256  symgfisg  19257  psgnunilem5  19283  lspsnat  20622  lsppratlem6  20629  lspprat  20630  lbsextlem4  20638  cnsubrg  20873  opsrtoslem2  21479  0ntr  22438  cmpfi  22775  dfconn2  22786  filconn  23250  cfinfil  23260  ufileu  23286  alexsublem  23411  ptcmplem2  23420  ptcmplem3  23421  restmetu  23942  reconnlem1  24205  bcthlem5  24708  itg10  25068  limcnlp  25258  noextendseq  27031  sltlpss  27258  upgrex  28085  uvtx01vtx  28387  ex-dif  29409  strlem1  31234  difininv  31486  eqdif  31488  difioo  31727  pmtrcnelor  31984  baselcarsg  32946  difelcarsg  32950  sibfof  32980  sitg0  32986  chtvalz  33282  onsucconni  34938  topdifinfeq  35850  nlpineqsn  35908  fdc  36233  setindtr  41377  oe0rif  41649  cantnfresb  41688  relnonrel  41933  inaex  42651  caragenunidm  44823
  Copyright terms: Public domain W3C validator