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

Theorem ssdif0 3727
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 3328 . . . 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 1615 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3335 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3642 . 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 1362    = wceq 1364    e. wcel 1757    \ cdif 3315    C_ wss 3318   (/)c0 3627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2966  df-dif 3321  df-in 3325  df-ss 3332  df-nul 3628
This theorem is referenced by:  vdif0  3728  difrab0eq  3729  pssdifn0  3730  difid  3737  difin0  3742  ordintdif  4757  dffv2  5754  fndifnfp  5896  tfi  6455  peano5  6490  tz7.49  6888  oe0m1  6951  sdomdif  7449  php3  7487  sucdom2  7497  isinf  7516  unxpwdom2  7793  fin23lem26  8484  fin23lem21  8498  fin1a2lem13  8571  zornn0g  8664  fpwwe2lem13  8799  fpwwe2  8800  isumltss  13296  rpnnen2  13493  symgsssg  15955  symgfisg  15956  psgnunilem5  15982  lspsnat  17150  lsppratlem6  17157  lspprat  17158  lbsextlem4  17166  opsrtoslem2  17500  cnsubrg  17719  0ntr  18519  cmpfi  18855  dfcon2  18867  filcon  19300  cfinfil  19310  ufileu  19336  alexsublem  19460  ptcmplem2  19469  ptcmplem3  19470  restmetu  20006  reconnlem1  20247  bcthlem5  20683  itg10  21010  limcnlp  21197  umgraex  23082  uvtx01vtx  23225  ex-dif  23455  strlem1  25479  difneqnul  25724  difioo  25897  sibfof  26576  sitg0  26582  probdif  26653  wfi  27517  frind  27553  wfrlem8  27580  wfrlem16  27588  symdifV  27705  onsucconi  28133  fdc  28487  setindtr  29220
  Copyright terms: Public domain W3C validator