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

Theorem ssdif0 3420
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
StepHypRef Expression
1 iman 415 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3088 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 304 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1554 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3092 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3376 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 270 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621    \ cdif 3075    C_ wss 3078   (/)c0 3362
This theorem is referenced by:  vdif0  3421  pssdifn0  3422  difid  3428  difin0  3433  ordintdif  4334  tfi  4535  peano5  4570  dffv2  5444  tz7.49  6343  oe0m1  6406  sdomdif  6894  php3  6932  sucdom2  6942  isinf  6961  unxpwdom2  7186  fin23lem26  7835  fin23lem21  7849  fin1a2lem13  7922  zornn0g  8016  fpwwe2lem13  8144  fpwwe2  8145  isumltss  12181  rpnnen2  12378  lspsnat  15732  lsppratlem6  15739  lspprat  15740  lbsextlem4  15746  opsrtoslem2  16058  cnsubrg  16264  0ntr  16640  cmpfi  16967  dfcon2  16977  filcon  17410  cfinfil  17420  ufileu  17446  alexsublem  17570  ptcmplem2  17579  ptcmplem3  17580  reconnlem1  18163  bcthlem5  18582  itg10  18875  limcnlp  19060  ex-dif  20623  strlem1  22660  umgraex  23046  wfi  23375  frind  23411  wfrlem8  23431  wfrlem16  23439  symdifV  23544  onsucconi  24050  fdc  25621  fndifnfp  25922  setindtr  26283  symgsssg  26574  symgfisg  26575  psgnunilem5  26583
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator