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

Theorem ssdif0 3622
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 414 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3266 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 303 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1572 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3273 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3578 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 269 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1717    \ cdif 3253    C_ wss 3256   (/)c0 3564
This theorem is referenced by:  vdif0  3623  difrab0eq  3624  pssdifn0  3625  difid  3632  difin0  3637  ordintdif  4564  tfi  4766  peano5  4801  dffv2  5728  tz7.49  6631  oe0m1  6694  sdomdif  7184  php3  7222  sucdom2  7232  isinf  7251  unxpwdom2  7482  fin23lem26  8131  fin23lem21  8145  fin1a2lem13  8218  zornn0g  8311  fpwwe2lem13  8443  fpwwe2  8444  isumltss  12548  rpnnen2  12745  lspsnat  16137  lsppratlem6  16144  lspprat  16145  lbsextlem4  16153  opsrtoslem2  16465  cnsubrg  16675  0ntr  17051  cmpfi  17386  dfcon2  17396  filcon  17829  cfinfil  17839  ufileu  17865  alexsublem  17989  ptcmplem2  17998  ptcmplem3  17999  restmetu  18482  reconnlem1  18721  bcthlem5  19143  itg10  19440  limcnlp  19625  umgraex  21218  uvtx01vtx  21360  ex-dif  21572  strlem1  23594  difneqnul  23834  difioo  23974  probdif  24450  wfi  25224  frind  25260  wfrlem8  25280  wfrlem16  25288  symdifV  25386  onsucconi  25894  fdc  26133  fndifnfp  26421  setindtr  26779  symgsssg  27070  symgfisg  27071  psgnunilem5  27079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-v 2894  df-dif 3259  df-in 3263  df-ss 3270  df-nul 3565
  Copyright terms: Public domain W3C validator