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

Theorem sseq0 3817
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 3526 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3816 . . 3  |-  ( A 
C_  (/)  ->  A  =  (/) )
31, 2syl6bi 228 . 2  |-  ( B  =  (/)  ->  ( A 
C_  B  ->  A  =  (/) ) )
43impcom 430 1  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    C_ wss 3476   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  ssn0  3818  ssdifin0  3908  disjxiun  4444  undom  7602  fieq0  7877  infdifsn  8069  cantnff  8089  tc00  8175  hashun3  12416  strlemor1  14578  strleun  14581  xpsc0  14811  xpsc1  14812  dmdprdsplit2lem  16884  2idlval  17663  opsrle  17911  pf1rcl  18156  ocvval  18465  pjfval  18504  en2top  19253  nrmsep  19624  isnrm3  19626  regsep2  19643  xkohaus  19889  kqdisj  19968  regr1lem  19975  alexsublem  20279  reconnlem1  21066  metdstri  21090  iundisj2  21694  clwlk0  24438  disjxpin  27120  iundisj2f  27122  iundisj2fi  27270  cvmsss2  28359  cldbnd  29721  cntotbnd  29895  mapfzcons1  30253  onfrALTlem2  32398  onfrALTlem2VD  32769
  Copyright terms: Public domain W3C validator