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

Theorem ssdif0 3823
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 3414 . . . 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 1691 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3421 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3747 . 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 1442    = wceq 1444    e. wcel 1887    \ cdif 3401    C_ wss 3404   (/)c0 3731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-v 3047  df-dif 3407  df-in 3411  df-ss 3418  df-nul 3732
This theorem is referenced by:  difn0  3824  vdif0  3825  difrab0eq  3826  pssdifn0  3827  difid  3835  difin0  3840  symdifv  4356  wfi  5413  ordintdif  5472  dffv2  5938  fndifnfp  6093  tfi  6680  peano5  6716  wfrlem8  7043  wfrlem16  7051  tz7.49  7162  oe0m1  7223  sdomdif  7720  php3  7758  sucdom2  7768  isinf  7785  unxpwdom2  8103  fin23lem26  8755  fin23lem21  8769  fin1a2lem13  8842  zornn0g  8935  fpwwe2lem13  9067  fpwwe2  9068  isumltss  13906  rpnnen2  14278  symgsssg  17108  symgfisg  17109  psgnunilem5  17135  lspsnat  18368  lsppratlem6  18375  lspprat  18376  lbsextlem4  18384  opsrtoslem2  18708  cnsubrg  19028  0ntr  20087  cmpfi  20423  dfcon2  20434  filcon  20898  cfinfil  20908  ufileu  20934  alexsublem  21059  ptcmplem2  21068  ptcmplem3  21069  restmetu  21585  reconnlem1  21844  bcthlem5  22296  itg10  22646  limcnlp  22833  umgraex  25050  uvtx01vtx  25220  ex-dif  25873  strlem1  27903  difioo  28364  baselcarsg  29138  difelcarsg  29142  sibfof  29173  sitg0  29179  frind  30481  onsucconi  31097  topdifinfeq  31753  fdc  32074  setindtr  35879  relnonrel  36193  caragenunidm  38329  upgrex  39184  uvtxa01vtx0  39469
  Copyright terms: Public domain W3C validator