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

Theorem ssdif0 3514
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 413 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3163 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 302 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1553 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3170 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3470 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 268 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1685    \ cdif 3150    C_ wss 3153   (/)c0 3456
This theorem is referenced by:  vdif0  3515  pssdifn0  3516  difid  3523  difin0  3528  ordintdif  4440  tfi  4643  peano5  4678  dffv2  5554  tz7.49  6453  oe0m1  6516  sdomdif  7005  php3  7043  sucdom2  7053  isinf  7072  unxpwdom2  7298  fin23lem26  7947  fin23lem21  7961  fin1a2lem13  8034  zornn0g  8128  fpwwe2lem13  8260  fpwwe2  8261  isumltss  12303  rpnnen2  12500  lspsnat  15894  lsppratlem6  15901  lspprat  15902  lbsextlem4  15910  opsrtoslem2  16222  cnsubrg  16428  0ntr  16804  cmpfi  17131  dfcon2  17141  filcon  17574  cfinfil  17584  ufileu  17610  alexsublem  17734  ptcmplem2  17743  ptcmplem3  17744  reconnlem1  18327  bcthlem5  18746  itg10  19039  limcnlp  19224  ex-dif  20787  strlem1  22826  umgraex  23282  wfi  23611  frind  23647  wfrlem8  23667  wfrlem16  23675  symdifV  23780  onsucconi  24286  fdc  25866  fndifnfp  26167  setindtr  26528  symgsssg  26819  symgfisg  26820  psgnunilem5  26828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457
  Copyright terms: Public domain W3C validator