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

Theorem ssdif0 3873
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 422 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3471 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 309 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1645 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3478 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3799 . 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 367   A.wal 1396    = wceq 1398    e. wcel 1823    \ cdif 3458    C_ wss 3461   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3784
This theorem is referenced by:  vdif0  3874  difrab0eq  3875  pssdifn0  3876  difid  3884  difin0  3889  symdifv  4393  ordintdif  4916  dffv2  5921  fndifnfp  6076  tfi  6661  peano5  6696  tz7.49  7102  oe0m1  7163  sdomdif  7658  php3  7696  sucdom2  7707  isinf  7726  unxpwdom2  8006  fin23lem26  8696  fin23lem21  8710  fin1a2lem13  8783  zornn0g  8876  fpwwe2lem13  9009  fpwwe2  9010  isumltss  13742  rpnnen2  14043  symgsssg  16691  symgfisg  16692  psgnunilem5  16718  lspsnat  17986  lsppratlem6  17993  lspprat  17994  lbsextlem4  18002  opsrtoslem2  18344  cnsubrg  18673  0ntr  19739  cmpfi  20075  dfcon2  20086  filcon  20550  cfinfil  20560  ufileu  20586  alexsublem  20710  ptcmplem2  20719  ptcmplem3  20720  restmetu  21256  reconnlem1  21497  bcthlem5  21933  itg10  22261  limcnlp  22448  umgraex  24525  uvtx01vtx  24694  ex-dif  25346  strlem1  27367  difneqnul  27614  difioo  27827  baselcarsg  28514  difelcarsg  28518  sibfof  28546  sitg0  28552  wfi  29527  frind  29563  wfrlem8  29590  wfrlem16  29598  onsucconi  30130  fdc  30478  setindtr  31205
  Copyright terms: Public domain W3C validator