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

Theorem sseq0 3661
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 3372 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3660 . . 3  |-  ( A 
C_  (/)  ->  A  =  (/) )
31, 2syl6bi 221 . 2  |-  ( B  =  (/)  ->  ( A 
C_  B  ->  A  =  (/) ) )
43impcom 421 1  |-  ( ( A  C_  B  /\  B  =  (/) )  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    C_ wss 3322   (/)c0 3630
This theorem is referenced by:  ssn0  3662  ssdifin0  3711  disjxiun  4211  undom  7198  fieq0  7428  infdifsn  7613  cantnff  7631  tc00  7689  hashun3  11660  strlemor1  13558  strleun  13561  xpsc0  13787  xpsc1  13788  dmdprdsplit2lem  15605  2idlval  16306  opsrle  16538  ocvval  16896  pjfval  16935  en2top  17052  nrmsep  17423  isnrm3  17425  regsep2  17442  xkohaus  17687  kqdisj  17766  regr1lem  17773  alexsublem  18077  reconnlem1  18859  metdstri  18883  iundisj2  19445  pf1rcl  19971  disjxpin  24030  iundisj2f  24032  iundisj2fi  24155  cvmsss2  24963  cldbnd  26331  cntotbnd  26507  mapfzcons1  26775  onfrALTlem2  28634  onfrALTlem2VD  29003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631
  Copyright terms: Public domain W3C validator