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

Theorem ssdif0 3688
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 415 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  ( x  e.  A  /\  -.  x  e.  B
) )
2 eldif 3332 . . . 4  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
31, 2xchbinxr 304 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  -.  x  e.  ( A 
\  B ) )
43albii 1576 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x  -.  x  e.  ( A  \  B ) )
5 dfss2 3339 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
6 eq0 3644 . 2  |-  ( ( A  \  B )  =  (/)  <->  A. x  -.  x  e.  ( A  \  B
) )
74, 5, 63bitr4i 270 1  |-  ( A 
C_  B  <->  ( A  \  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360   A.wal 1550    = wceq 1653    e. wcel 1726    \ cdif 3319    C_ wss 3322   (/)c0 3630
This theorem is referenced by:  vdif0  3689  difrab0eq  3690  pssdifn0  3691  difid  3698  difin0  3703  ordintdif  4632  tfi  4835  peano5  4870  dffv2  5798  tz7.49  6704  oe0m1  6767  sdomdif  7257  php3  7295  sucdom2  7305  isinf  7324  unxpwdom2  7558  fin23lem26  8207  fin23lem21  8221  fin1a2lem13  8294  zornn0g  8387  fpwwe2lem13  8519  fpwwe2  8520  isumltss  12630  rpnnen2  12827  lspsnat  16219  lsppratlem6  16226  lspprat  16227  lbsextlem4  16235  opsrtoslem2  16547  cnsubrg  16761  0ntr  17137  cmpfi  17473  dfcon2  17484  filcon  17917  cfinfil  17927  ufileu  17953  alexsublem  18077  ptcmplem2  18086  ptcmplem3  18087  restmetu  18619  reconnlem1  18859  bcthlem5  19283  itg10  19582  limcnlp  19767  umgraex  21360  uvtx01vtx  21503  ex-dif  21733  strlem1  23755  difneqnul  23999  difioo  24147  sibfof  24656  probdif  24680  wfi  25484  frind  25520  wfrlem8  25547  wfrlem16  25555  symdifV  25672  onsucconi  26189  fdc  26451  fndifnfp  26739  setindtr  27097  symgsssg  27387  symgfisg  27388  psgnunilem5  27396
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631
  Copyright terms: Public domain W3C validator