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

Theorem sseq0 3657
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 3366 . . 3  |-  ( B  =  (/)  ->  ( A 
C_  B  <->  A  C_  (/) ) )
2 ss0 3656 . . 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 1362    C_ wss 3316   (/)c0 3625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330  df-nul 3626
This theorem is referenced by:  ssn0  3658  ssdifin0  3748  disjxiun  4277  undom  7387  fieq0  7659  infdifsn  7850  cantnff  7870  tc00  7956  hashun3  12130  strlemor1  14247  strleun  14250  xpsc0  14480  xpsc1  14481  dmdprdsplit2lem  16517  2idlval  17236  opsrle  17488  ocvval  17933  pjfval  17972  en2top  18431  nrmsep  18802  isnrm3  18804  regsep2  18821  xkohaus  19067  kqdisj  19146  regr1lem  19153  alexsublem  19457  reconnlem1  20244  metdstri  20268  iundisj2  20871  pf1rcl  21399  disjxpin  25753  iundisj2f  25755  iundisj2fi  25903  cvmsss2  27010  cldbnd  28362  cntotbnd  28536  mapfzcons1  28895  clwlk0  30268  onfrALTlem2  30952  onfrALTlem2VD  31324
  Copyright terms: Public domain W3C validator