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

Theorem ss0b 3765
Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
Assertion
Ref Expression
ss0b  |-  ( A 
C_  (/)  <->  A  =  (/) )

Proof of Theorem ss0b
StepHypRef Expression
1 0ss 3764 . . 3  |-  (/)  C_  A
2 eqss 3469 . . 3  |-  ( A  =  (/)  <->  ( A  C_  (/) 
/\  (/)  C_  A )
)
31, 2mpbiran2 910 . 2  |-  ( A  =  (/)  <->  A  C_  (/) )
43bicomi 202 1  |-  ( A 
C_  (/)  <->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370    C_ wss 3426   (/)c0 3735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-dif 3429  df-in 3433  df-ss 3440  df-nul 3736
This theorem is referenced by:  ss0  3766  un00  3812  ssdisj  3826  pw0  4118  fnsuppeq0OLD  6038  fnsuppeq0  6817  cnfcom2lem  8035  cnfcom2lemOLD  8043  card0  8229  kmlem5  8424  cf0  8521  fin1a2lem12  8681  mreexexlem3d  14686  efgval  16318  ppttop  18727  0nnei  18832  disjunsn  26070  isarchi  26333  filnetlem4  28740  pnonsingN  33883  osumcllem4N  33909
  Copyright terms: Public domain W3C validator