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

Theorem ssdif0 3885
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 424 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3486 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 311 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1620 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3493 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3800 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 277 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1377    = wceq 1379    e. wcel 1767    \ cdif 3473    C_ wss 3476   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  vdif0  3886  difrab0eq  3887  pssdifn0  3888  difid  3895  difin0  3900  ordintdif  4927  dffv2  5940  fndifnfp  6090  tfi  6672  peano5  6707  tz7.49  7110  oe0m1  7171  sdomdif  7665  php3  7703  sucdom2  7714  isinf  7733  unxpwdom2  8014  fin23lem26  8705  fin23lem21  8719  fin1a2lem13  8792  zornn0g  8885  fpwwe2lem13  9020  fpwwe2  9021  isumltss  13623  rpnnen2  13820  symgsssg  16298  symgfisg  16299  psgnunilem5  16325  lspsnat  17591  lsppratlem6  17598  lspprat  17599  lbsextlem4  17607  opsrtoslem2  17948  cnsubrg  18274  0ntr  19366  cmpfi  19702  dfcon2  19714  filcon  20147  cfinfil  20157  ufileu  20183  alexsublem  20307  ptcmplem2  20316  ptcmplem3  20317  restmetu  20853  reconnlem1  21094  bcthlem5  21530  itg10  21858  limcnlp  22045  umgraex  24027  uvtx01vtx  24196  ex-dif  24849  strlem1  26873  difneqnul  27117  difioo  27289  sibfof  27950  sitg0  27956  probdif  28027  wfi  28892  frind  28928  wfrlem8  28955  wfrlem16  28963  symdifV  29080  onsucconi  29507  fdc  29869  setindtr  30598
  Copyright terms: Public domain W3C validator