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

Theorem sseq0 3486
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 3200 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3485 . . 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 1623    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  ssn0  3487  ssdifin0  3535  disjxiun  4020  undom  6950  fieq0  7174  infdifsn  7357  cantnff  7375  tc00  7433  hashun3  11366  strlemor1  13235  strleun  13238  xpsc0  13462  xpsc1  13463  dmdprdsplit2lem  15280  2idlval  15985  opsrle  16217  ocvval  16567  pjfval  16606  en2top  16723  nrmsep  17085  isnrm3  17087  regsep2  17104  xkohaus  17347  kqdisj  17423  regr1lem  17430  alexsublem  17738  reconnlem1  18331  metdstri  18355  iundisj2  18906  pf1rcl  19432  iundisj2fi  23364  iundisj2f  23366  cvmsss2  23805  cldifemp  25524  cldbnd  26244  cntotbnd  26520  mapfzcons1  26794  onfrALTlem2  28311  onfrALTlem2VD  28665
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator