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

Theorem sseq0 3734
Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
sseq0  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )

Proof of Theorem sseq0
StepHypRef Expression
1 sseq2 3424 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3733 . . 3  |-  ( A 
C_  (/)  ->  A  =  (/) )
31, 2syl6bi 231 . 2  |-  ( B  =  (/)  ->  ( A 
C_  B  ->  A  =  (/) ) )
43impcom 431 1  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    C_ wss 3374   (/)c0 3699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-dif 3377  df-in 3381  df-ss 3388  df-nul 3700
This theorem is referenced by:  ssn0  3735  ssdifin0  3817  disjxiun  4358  undom  7608  fieq0  7883  infdifsn  8109  cantnff  8126  tc00  8179  hashun3  12508  strlemor1  15155  strleun  15158  xpsc0  15404  xpsc1  15405  dmdprdsplit2lem  17616  2idlval  18395  opsrle  18637  pf1rcl  18875  ocvval  19167  pjfval  19206  en2top  19938  nrmsep  20310  isnrm3  20312  regsep2  20329  xkohaus  20605  kqdisj  20684  regr1lem  20691  alexsublem  20996  reconnlem1  21781  metdstri  21805  metdstriOLD  21820  iundisj2  22439  clwlk0  25427  disjxpin  28139  iundisj2f  28141  iundisj2fi  28318  cvmsss2  29944  cldbnd  30926  cntotbnd  32035  mapfzcons1  35471  onfrALTlem2  36825  onfrALTlem2VD  37202  nnuzdisj  37475
  Copyright terms: Public domain W3C validator