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

Theorem ssdif0 3526
Description: Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
ssdif0  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )

Proof of Theorem ssdif0
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 iman 413 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3175 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 302 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1556 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3182 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3482 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 268 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696    \ cdif 3162    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  vdif0  3527  pssdifn0  3528  difid  3535  difin0  3540  ordintdif  4457  tfi  4660  peano5  4695  dffv2  5608  tz7.49  6473  oe0m1  6536  sdomdif  7025  php3  7063  sucdom2  7073  isinf  7092  unxpwdom2  7318  fin23lem26  7967  fin23lem21  7981  fin1a2lem13  8054  zornn0g  8148  fpwwe2lem13  8280  fpwwe2  8281  isumltss  12323  rpnnen2  12520  lspsnat  15914  lsppratlem6  15921  lspprat  15922  lbsextlem4  15930  opsrtoslem2  16242  cnsubrg  16448  0ntr  16824  cmpfi  17151  dfcon2  17161  filcon  17594  cfinfil  17604  ufileu  17630  alexsublem  17754  ptcmplem2  17763  ptcmplem3  17764  reconnlem1  18347  bcthlem5  18766  itg10  19059  limcnlp  19244  ex-dif  20826  strlem1  22846  difneqnul  23143  difioo  23290  probdif  23638  umgraex  23890  wfi  24278  frind  24314  wfrlem8  24334  wfrlem16  24342  symdifV  24440  onsucconi  24948  fdc  26558  fndifnfp  26859  setindtr  27220  symgsssg  27511  symgfisg  27512  psgnunilem5  27520  uvtx01vtx  28305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator