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

Theorem sseli 2969
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1 𝐴𝐵
Assertion
Ref Expression
sseli (𝐶𝐴𝐶𝐵)

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2 𝐴𝐵
2 ssel 2967 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 7 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  sselii  2970  sseldi  2971  elun1  3138  elun2  3139  finds  4351  finds2  4352  issref  4735  2elresin  5038  fvun1  5267  fvmptssdm  5283  fvimacnvi  5309  elpreima  5314  ofrfval  5748  fnofval  5749  off  5752  offres  5790  eqopi  5826  op1steq  5833  dfoprab4  5846  f1od2  5884  reldmtpos  5899  smores3  5939  smores2  5940  pinn  6465  indpi  6498  enq0enq  6587  preqlu  6628  elinp  6630  prop  6631  elnp1st2nd  6632  prarloclem5  6656  cauappcvgprlemladd  6814  peano5nnnn  7024  nnindnn  7025  recn  7072  rexr  7130  peano5nni  7993  nnre  7997  nncn  7998  nnind  8006  nnnn0  8246  nn0re  8248  nn0cn  8249  nnz  8321  nn0z  8322  nnq  8665  qcn  8666  rpre  8687  iccshftri  8964  iccshftli  8966  iccdili  8968  icccntri  8970  fzval2  8979  fzelp1  9038  4fvwrd4  9099  elfzo1  9148  expcllem  9431  expcl2lemap  9432  m1expcl2  9442  bcm1k  9628  bcpasc  9634  cau3lem  9941  climconst2  10043  dvdsflip  10163
  Copyright terms: Public domain W3C validator