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

Proof of Theorem sseq0

Step	Hyp	Ref	Expression
1		sseq2 3525	. . 3
2		ss0 3816	. . 3
3	1, 2	syl6bi 228	. 2
4	3	impcom 430	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  c0 3784

This theorem is referenced by:  ssn0  3818  ssdifin0  3909  disjxiun  4449  undom  7625  fieq0  7901  infdifsn  8094  cantnff  8114  tc00  8200  hashun3  12452  strlemor1  14724  strleun  14727  xpsc0  14957  xpsc1  14958  dmdprdsplit2lem  17094  2idlval  17881  opsrle  18140  pf1rcl  18385  ocvval  18698  pjfval  18737  en2top  19487  nrmsep  19858  isnrm3  19860  regsep2  19877  xkohaus  20154  kqdisj  20233  regr1lem  20240  alexsublem  20544  reconnlem1  21331  metdstri  21355  iundisj2  21959  clwlk0  24762  disjxpin  27447  iundisj2f  27449  iundisj2fi  27602  cvmsss2  28719  cldbnd  30144  cntotbnd  30292  mapfzcons1  30649  onfrALTlem2  33318  onfrALTlem2VD  33689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785