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

Theorem sseli 2938
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1 AB
Assertion
Ref Expression
sseli (𝐶 A𝐶 B)

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2 AB
2 ssel 2936 . 2 (AB → (𝐶 A𝐶 B))
31, 2ax-mp 7 1 (𝐶 A𝐶 B)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1393  wss 2914
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2921  df-ss 2928
This theorem is referenced by:  sselii  2939  sseldi  2940  elun1  3107  elun2  3108  finds  4269  finds2  4270  issref  4653  2elresin  4956  fvun1  5185  fvmptssdm  5201  fvimacnvi  5227  elpreima  5232  ofrfval  5665  fnofval  5666  off  5669  offres  5707  eqopi  5743  op1steq  5750  dfoprab4  5763  reldmtpos  5813  smores3  5853  smores2  5854  pinn  6297  indpi  6330  enq0enq  6419  preqlu  6460  elinp  6462  prop  6463  elnp1st2nd  6464  prarloclem5  6488  cauappcvgprlemladd  6646  peano5nnnn  6856  nnindnn  6857  recn  6904  rexr  6960  peano5nni  7790  nnre  7794  nncn  7795  nnind  7803  nnnn0  8056  nn0re  8058  nn0cn  8059  nnz  8132  nn0z  8133  nnq  8436  qcn  8437  rpre  8456  iccshftri  8725  iccshftli  8727  iccdili  8729  icccntri  8731  fzval2  8739  fzelp1  8798  4fvwrd4  8859  elfzo1  8908  expcllem  9013  expcl2lemap  9014  m1expcl2  9024
  Copyright terms: Public domain W3C validator