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

Theorem sseq0 3499
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 3213 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3498 . . 3  |-  ( A 
C_  (/)  ->  A  =  (/) )
31, 2syl6bi 219 . 2  |-  ( B  =  (/)  ->  ( A 
C_  B  ->  A  =  (/) ) )
43impcom 419 1  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  ssn0  3500  ssdifin0  3548  disjxiun  4036  undom  6966  fieq0  7190  infdifsn  7373  cantnff  7391  tc00  7449  hashun3  11382  strlemor1  13251  strleun  13254  xpsc0  13478  xpsc1  13479  dmdprdsplit2lem  15296  2idlval  16001  opsrle  16233  ocvval  16583  pjfval  16622  en2top  16739  nrmsep  17101  isnrm3  17103  regsep2  17120  xkohaus  17363  kqdisj  17439  regr1lem  17446  alexsublem  17754  reconnlem1  18347  metdstri  18371  iundisj2  18922  pf1rcl  19448  iundisj2fi  23379  iundisj2f  23381  cvmsss2  23820  cldifemp  25627  cldbnd  26347  cntotbnd  26623  mapfzcons1  26897  onfrALTlem2  28610  onfrALTlem2VD  28981
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator