ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseli Unicode version

Theorem sseli 3061
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1  |-  A  C_  B
Assertion
Ref Expression
sseli  |-  ( C  e.  A  ->  C  e.  B )

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2  |-  A  C_  B
2 ssel 3059 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2ax-mp 5 1  |-  ( C  e.  A  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463    C_ wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sselii  3062  sseldi  3063  elun1  3211  elun2  3212  finds  4482  finds2  4483  issref  4889  2elresin  5202  fvun1  5453  fvmptssdm  5471  elfvmptrab1  5481  fvimacnvi  5500  elpreima  5505  ofrfval  5956  ofvalg  5957  off  5960  offres  5999  eqopi  6036  op1steq  6043  dfoprab4  6056  f1od2  6098  reldmtpos  6116  smores3  6156  smores2  6157  ctssdccl  6962  pinn  7081  indpi  7114  enq0enq  7203  preqlu  7244  elinp  7246  prop  7247  elnp1st2nd  7248  prarloclem5  7272  cauappcvgprlemladd  7430  peano5nnnn  7664  nnindnn  7665  recn  7717  rexr  7775  peano5nni  8680  nnre  8684  nncn  8685  nnind  8693  nnnn0  8935  nn0re  8937  nn0cn  8938  nn0xnn0  8995  nnz  9024  nn0z  9025  nnq  9374  qcn  9375  rpre  9396  iccshftri  9718  iccshftli  9720  iccdili  9722  icccntri  9724  fzval2  9733  fzelp1  9794  4fvwrd4  9857  elfzo1  9907  expcllem  10244  expcl2lemap  10245  m1expcl2  10255  bcm1k  10446  bcpasc  10452  cau3lem  10826  climconst2  11000  fsum3  11096  binomlem  11192  dvdsflip  11445  infssuzcldc  11540  isprm3  11695  phimullem  11796  structcnvcnv  11870  fvsetsid  11888  tgval2  12115  qtopbasss  12585  exmidsbthrlem  13019
  Copyright terms: Public domain W3C validator