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

Theorem ssdif0 3488
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 3137 . . . 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 3144 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3444 . 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 3124    C_ wss 3127   (/)c0 3430
This theorem is referenced by:  vdif0  3489  pssdifn0  3490  difid  3497  difin0  3502  ordintdif  4413  tfi  4616  peano5  4651  dffv2  5526  tz7.49  6425  oe0m1  6488  sdomdif  6977  php3  7015  sucdom2  7025  isinf  7044  unxpwdom2  7270  fin23lem26  7919  fin23lem21  7933  fin1a2lem13  8006  zornn0g  8100  fpwwe2lem13  8232  fpwwe2  8233  isumltss  12270  rpnnen2  12467  lspsnat  15861  lsppratlem6  15868  lspprat  15869  lbsextlem4  15877  opsrtoslem2  16189  cnsubrg  16395  0ntr  16771  cmpfi  17098  dfcon2  17108  filcon  17541  cfinfil  17551  ufileu  17577  alexsublem  17701  ptcmplem2  17710  ptcmplem3  17711  reconnlem1  18294  bcthlem5  18713  itg10  19006  limcnlp  19191  ex-dif  20754  strlem1  22791  umgraex  23248  wfi  23577  frind  23613  wfrlem8  23633  wfrlem16  23641  symdifV  23746  onsucconi  24252  fdc  25823  fndifnfp  26124  setindtr  26485  symgsssg  26776  symgfisg  26777  psgnunilem5  26785
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator