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

Theorem ssdif0 3895
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 438 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
2 eldif 3549 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2xchbinxr 323 . . 3 ((𝑥𝐴𝑥𝐵) ↔ ¬ 𝑥 ∈ (𝐴𝐵))
43albii 1736 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
5 dfss2 3556 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
6 eq0 3887 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴𝐵))
74, 5, 63bitr4i 290 1 (𝐴𝐵 ↔ (𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wcel 1976  cdif 3536  wss 3539  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874
This theorem is referenced by:  difn0  3896  pssdifn0  3897  difid  3901  vdif0  3988  difrab0eq  3989  difin0  3992  symdifv  4528  wfi  5615  ordintdif  5676  dffv2  6165  fndifnfp  6324  tfi  6922  peano5  6958  wfrlem8  7286  wfrlem16  7294  tz7.49  7404  oe0m1  7465  sdomdif  7970  php3  8008  sucdom2  8018  isinf  8035  unxpwdom2  8353  fin23lem26  9007  fin23lem21  9021  fin1a2lem13  9094  zornn0g  9187  fpwwe2lem13  9320  fpwwe2  9321  isumltss  14367  rpnnen2lem12  14741  symgsssg  17658  symgfisg  17659  psgnunilem5  17685  lspsnat  18914  lsppratlem6  18921  lspprat  18922  lbsextlem4  18930  opsrtoslem2  19254  cnsubrg  19573  0ntr  20632  cmpfi  20968  dfcon2  20979  filcon  21444  cfinfil  21454  ufileu  21480  alexsublem  21605  ptcmplem2  21614  ptcmplem3  21615  restmetu  22132  reconnlem1  22384  bcthlem5  22877  itg10  23205  limcnlp  23392  umgraex  25645  uvtx01vtx  25813  ex-dif  26465  strlem1  28286  difioo  28727  baselcarsg  29488  difelcarsg  29492  sibfof  29522  sitg0  29528  frind  30777  onsucconi  31399  topdifinfeq  32157  fdc  32494  setindtr  36392  relnonrel  36695  caragenunidm  39181  upgrex  40299  uvtxa01vtx0  40604
  Copyright terms: Public domain W3C validator