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

Theorem ssdif0 3455
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 3104 . . . 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 3111 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3411 . 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 3091    C_ wss 3094   (/)c0 3397
This theorem is referenced by:  vdif0  3456  pssdifn0  3457  difid  3464  difin0  3469  ordintdif  4378  tfi  4581  peano5  4616  dffv2  5491  tz7.49  6390  oe0m1  6453  sdomdif  6942  php3  6980  sucdom2  6990  isinf  7009  unxpwdom2  7235  fin23lem26  7884  fin23lem21  7898  fin1a2lem13  7971  zornn0g  8065  fpwwe2lem13  8197  fpwwe2  8198  isumltss  12234  rpnnen2  12431  lspsnat  15825  lsppratlem6  15832  lspprat  15833  lbsextlem4  15841  opsrtoslem2  16153  cnsubrg  16359  0ntr  16735  cmpfi  17062  dfcon2  17072  filcon  17505  cfinfil  17515  ufileu  17541  alexsublem  17665  ptcmplem2  17674  ptcmplem3  17675  reconnlem1  18258  bcthlem5  18677  itg10  18970  limcnlp  19155  ex-dif  20718  strlem1  22755  umgraex  23212  wfi  23541  frind  23577  wfrlem8  23597  wfrlem16  23605  symdifV  23710  onsucconi  24216  fdc  25787  fndifnfp  26088  setindtr  26449  symgsssg  26740  symgfisg  26741  psgnunilem5  26749
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398
  Copyright terms: Public domain W3C validator