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

Theorem sseq0 3771
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 3464 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3770 . . 3  |-  ( A 
C_  (/)  ->  A  =  (/) )
31, 2syl6bi 228 . 2  |-  ( B  =  (/)  ->  ( A 
C_  B  ->  A  =  (/) ) )
43impcom 428 1  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    C_ wss 3414   (/)c0 3738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-dif 3417  df-in 3421  df-ss 3428  df-nul 3739
This theorem is referenced by:  ssn0  3772  ssdifin0  3853  disjxiun  4392  undom  7643  fieq0  7915  infdifsn  8106  cantnff  8125  tc00  8211  hashun3  12500  strlemor1  14936  strleun  14939  xpsc0  15174  xpsc1  15175  dmdprdsplit2lem  17414  2idlval  18201  opsrle  18460  pf1rcl  18705  ocvval  18996  pjfval  19035  en2top  19779  nrmsep  20151  isnrm3  20153  regsep2  20170  xkohaus  20446  kqdisj  20525  regr1lem  20532  alexsublem  20836  reconnlem1  21623  metdstri  21647  iundisj2  22251  clwlk0  25179  disjxpin  27880  iundisj2f  27882  iundisj2fi  28050  cvmsss2  29571  cldbnd  30554  cntotbnd  31574  mapfzcons1  35011  onfrALTlem2  36342  onfrALTlem2VD  36720
  Copyright terms: Public domain W3C validator