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

Theorem ssdif0 3737
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 3338 . . . 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 1610 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3345 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3652 . 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 1367    = wceq 1369    e. wcel 1756    \ cdif 3325    C_ wss 3328   (/)c0 3637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2974  df-dif 3331  df-in 3335  df-ss 3342  df-nul 3638
This theorem is referenced by:  vdif0  3738  difrab0eq  3739  pssdifn0  3740  difid  3747  difin0  3752  ordintdif  4768  dffv2  5764  fndifnfp  5907  tfi  6464  peano5  6499  tz7.49  6900  oe0m1  6961  sdomdif  7459  php3  7497  sucdom2  7507  isinf  7526  unxpwdom2  7803  fin23lem26  8494  fin23lem21  8508  fin1a2lem13  8581  zornn0g  8674  fpwwe2lem13  8809  fpwwe2  8810  isumltss  13311  rpnnen2  13508  symgsssg  15973  symgfisg  15974  psgnunilem5  16000  lspsnat  17226  lsppratlem6  17233  lspprat  17234  lbsextlem4  17242  opsrtoslem2  17566  cnsubrg  17873  0ntr  18675  cmpfi  19011  dfcon2  19023  filcon  19456  cfinfil  19466  ufileu  19492  alexsublem  19616  ptcmplem2  19625  ptcmplem3  19626  restmetu  20162  reconnlem1  20403  bcthlem5  20839  itg10  21166  limcnlp  21353  umgraex  23257  uvtx01vtx  23400  ex-dif  23630  strlem1  25654  difneqnul  25898  difioo  26072  sibfof  26726  sitg0  26732  probdif  26803  wfi  27668  frind  27704  wfrlem8  27731  wfrlem16  27739  symdifV  27856  onsucconi  28283  fdc  28641  setindtr  29373
  Copyright terms: Public domain W3C validator