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

Theorem ssdif0 4322
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 402 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 eldif 3945 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 336 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1811 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3954 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 4307 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 304 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wcel 2105  cdif 3932  wss 3935  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-in 3942  df-ss 3951  df-nul 4291
This theorem is referenced by:  difn0  4323  pssdifn0  4324  difid  4329  vdif0  4416  difrab0eq  4417  difin0  4420  symdifv  5000  wfi  6175  ordintdif  6234  dffv2  6750  fndifnfp  6931  tfi  7556  peano5  7593  wfrlem8  7953  wfrlem16  7961  tz7.49  8072  oe0m1  8137  sdomdif  8654  php3  8692  sucdom2  8703  isinf  8720  unxpwdom2  9041  fin23lem26  9736  fin23lem21  9750  fin1a2lem13  9823  zornn0g  9916  fpwwe2lem13  10053  fpwwe2  10054  isumltss  15193  rpnnen2lem12  15568  symgsssg  18526  symgfisg  18527  psgnunilem5  18553  lspsnat  19848  lsppratlem6  19855  lspprat  19856  lbsextlem4  19864  opsrtoslem2  20195  cnsubrg  20535  0ntr  21609  cmpfi  21946  dfconn2  21957  filconn  22421  cfinfil  22431  ufileu  22457  alexsublem  22582  ptcmplem2  22591  ptcmplem3  22592  restmetu  23109  reconnlem1  23363  bcthlem5  23860  itg10  24218  limcnlp  24405  upgrex  26805  uvtx01vtx  27107  ex-dif  28130  strlem1  29955  difininv  30207  eqdif  30209  difioo  30432  pmtrcnelor  30663  baselcarsg  31464  difelcarsg  31468  sibfof  31498  sitg0  31504  chtvalz  31800  frpoind  32978  frind  32983  frrlem13  33033  frrlem14  33034  noextendseq  33072  onsucconni  33683  topdifinfeq  34514  nlpineqsn  34572  fdc  34903  setindtr  39501  relnonrel  39827  inaex  40513  caragenunidm  42671
  Copyright terms: Public domain W3C validator