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

Theorem ssdif0 3513
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 3162 . . . 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 3169 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3469 . 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 1684    \ cdif 3149    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  vdif0  3514  pssdifn0  3515  difid  3522  difin0  3527  ordintdif  4441  tfi  4644  peano5  4679  dffv2  5592  tz7.49  6457  oe0m1  6520  sdomdif  7009  php3  7047  sucdom2  7057  isinf  7076  unxpwdom2  7302  fin23lem26  7951  fin23lem21  7965  fin1a2lem13  8038  zornn0g  8132  fpwwe2lem13  8264  fpwwe2  8265  isumltss  12307  rpnnen2  12504  lspsnat  15898  lsppratlem6  15905  lspprat  15906  lbsextlem4  15914  opsrtoslem2  16226  cnsubrg  16432  0ntr  16808  cmpfi  17135  dfcon2  17145  filcon  17578  cfinfil  17588  ufileu  17614  alexsublem  17738  ptcmplem2  17747  ptcmplem3  17748  reconnlem1  18331  bcthlem5  18750  itg10  19043  limcnlp  19228  ex-dif  20810  strlem1  22830  difneqnul  23127  difioo  23275  probdif  23623  umgraex  23875  wfi  24207  frind  24243  wfrlem8  24263  wfrlem16  24271  symdifV  24369  onsucconi  24876  fdc  26455  fndifnfp  26756  setindtr  27117  symgsssg  27408  symgfisg  27409  psgnunilem5  27417  uvtx01vtx  28164
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator