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

Theorem ssdif0 3515
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 3164 . . . 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 1555 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3171 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3471 . 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 1529    = wceq 1625    e. wcel 1686    \ cdif 3151    C_ wss 3154   (/)c0 3457
This theorem is referenced by:  vdif0  3516  pssdifn0  3517  difid  3524  difin0  3529  ordintdif  4443  tfi  4646  peano5  4681  dffv2  5594  tz7.49  6459  oe0m1  6522  sdomdif  7011  php3  7049  sucdom2  7059  isinf  7078  unxpwdom2  7304  fin23lem26  7953  fin23lem21  7967  fin1a2lem13  8040  zornn0g  8134  fpwwe2lem13  8266  fpwwe2  8267  isumltss  12309  rpnnen2  12506  lspsnat  15900  lsppratlem6  15907  lspprat  15908  lbsextlem4  15916  opsrtoslem2  16228  cnsubrg  16434  0ntr  16810  cmpfi  17137  dfcon2  17147  filcon  17580  cfinfil  17590  ufileu  17616  alexsublem  17740  ptcmplem2  17749  ptcmplem3  17750  reconnlem1  18333  bcthlem5  18752  itg10  19045  limcnlp  19230  ex-dif  20812  strlem1  22832  difneqnul  23129  difioo  23277  probdif  23625  umgraex  23877  wfi  24209  frind  24245  wfrlem8  24265  wfrlem16  24273  symdifV  24371  onsucconi  24878  fdc  26466  fndifnfp  26767  setindtr  27128  symgsssg  27419  symgfisg  27420  psgnunilem5  27428  uvtx01vtx  28175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator