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

Theorem sseli 3151
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 3149 . 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 2148    C_ wss 3129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142
This theorem is referenced by:  sselii  3152  sselid  3153  elun1  3302  elun2  3303  finds  4595  finds2  4596  issref  5006  2elresin  5322  fvun1  5577  fvmptssdm  5595  elfvmptrab1  5605  fvimacnvi  5625  elpreima  5630  ofrfval  6084  ofvalg  6085  off  6088  offres  6129  eqopi  6166  op1steq  6173  dfoprab4  6186  f1od2  6229  reldmtpos  6247  smores3  6287  smores2  6288  ctssdccl  7103  pinn  7286  indpi  7319  enq0enq  7408  preqlu  7449  elinp  7451  prop  7452  elnp1st2nd  7453  prarloclem5  7477  cauappcvgprlemladd  7635  peano5nnnn  7869  nnindnn  7870  recn  7922  rexr  7980  peano5nni  8898  nnre  8902  nncn  8903  nnind  8911  nnnn0  9159  nn0re  9161  nn0cn  9162  nn0xnn0  9219  nnz  9248  nn0z  9249  nnq  9609  qcn  9610  rpre  9634  iccshftri  9969  iccshftli  9971  iccdili  9973  icccntri  9975  fzval2  9985  fzelp1  10047  4fvwrd4  10113  elfzo1  10163  expcllem  10504  expcl2lemap  10505  m1expcl2  10515  bcm1k  10711  bcpasc  10717  cau3lem  11094  climconst2  11270  fsum3  11366  binomlem  11462  fprodge1  11618  cos12dec  11746  dvdsflip  11827  infssuzcldc  11922  isprm3  12088  phimullem  12195  prmdiveq  12206  structcnvcnv  12448  fvsetsid  12466  tgval2  13184  qtopbasss  13654  dedekindicc  13744  ivthinc  13754  ivthdec  13755  cosz12  13834  cos0pilt1  13906  ioocosf1o  13908  exmidsbthrlem  14393
  Copyright terms: Public domain W3C validator