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

Theorem ssdif0 3852
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 426 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3447 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 313 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1688 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3454 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3778 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 281 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1436    = wceq 1438    e. wcel 1869    \ cdif 3434    C_ wss 3437   (/)c0 3762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-v 3084  df-dif 3440  df-in 3444  df-ss 3451  df-nul 3763
This theorem is referenced by:  difn0  3853  vdif0  3854  difrab0eq  3855  pssdifn0  3856  difid  3864  difin0  3869  symdifv  4375  wfi  5430  ordintdif  5489  dffv2  5952  fndifnfp  6106  tfi  6692  peano5  6728  wfrlem8  7049  wfrlem16  7057  tz7.49  7168  oe0m1  7229  sdomdif  7724  php3  7762  sucdom2  7772  isinf  7789  unxpwdom2  8107  fin23lem26  8757  fin23lem21  8771  fin1a2lem13  8844  zornn0g  8937  fpwwe2lem13  9069  fpwwe2  9070  isumltss  13899  rpnnen2  14271  symgsssg  17101  symgfisg  17102  psgnunilem5  17128  lspsnat  18361  lsppratlem6  18368  lspprat  18369  lbsextlem4  18377  opsrtoslem2  18701  cnsubrg  19021  0ntr  20079  cmpfi  20415  dfcon2  20426  filcon  20890  cfinfil  20900  ufileu  20926  alexsublem  21051  ptcmplem2  21060  ptcmplem3  21061  restmetu  21577  reconnlem1  21836  bcthlem5  22288  itg10  22638  limcnlp  22825  umgraex  25042  uvtx01vtx  25212  ex-dif  25865  strlem1  27895  difioo  28364  baselcarsg  29140  difelcarsg  29144  sibfof  29175  sitg0  29181  frind  30482  onsucconi  31096  topdifinfeq  31711  fdc  32032  setindtr  35843  caragenunidm  38152  umgrex  38889
  Copyright terms: Public domain W3C validator