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

Theorem sseq0 3769
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 3478 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3768 . . 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 1370    C_ wss 3428   (/)c0 3737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-dif 3431  df-in 3435  df-ss 3442  df-nul 3738
This theorem is referenced by:  ssn0  3770  ssdifin0  3860  disjxiun  4389  undom  7501  fieq0  7774  infdifsn  7965  cantnff  7985  tc00  8071  hashun3  12251  strlemor1  14369  strleun  14372  xpsc0  14602  xpsc1  14603  dmdprdsplit2lem  16651  2idlval  17423  opsrle  17666  pf1rcl  17894  ocvval  18203  pjfval  18242  en2top  18708  nrmsep  19079  isnrm3  19081  regsep2  19098  xkohaus  19344  kqdisj  19423  regr1lem  19430  alexsublem  19734  reconnlem1  20521  metdstri  20545  iundisj2  21148  disjxpin  26066  iundisj2f  26068  iundisj2fi  26217  cvmsss2  27299  cldbnd  28661  cntotbnd  28835  mapfzcons1  29193  clwlk0  30565  onfrALTlem2  31556  onfrALTlem2VD  31927
  Copyright terms: Public domain W3C validator