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

Theorem sseli 2935
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 2933 . 2 (AB → (𝐶 A𝐶 B))
31, 2ax-mp 7 1 (𝐶 A𝐶 B)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  wss 2911
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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925
This theorem is referenced by:  sselii  2936  sseldi  2937  elun1  3104  elun2  3105  finds  4266  finds2  4267  issref  4650  2elresin  4953  fvun1  5182  fvmptssdm  5198  fvimacnvi  5224  elpreima  5229  ofrfval  5662  fnofval  5663  off  5666  offres  5704  eqopi  5740  op1steq  5747  dfoprab4  5760  reldmtpos  5809  smores3  5849  smores2  5850  pinn  6293  indpi  6326  enq0enq  6414  preqlu  6455  elinp  6457  prop  6458  elnp1st2nd  6459  prarloclem5  6483  cauappcvgprlemladd  6630  recn  6812  rexr  6868  peano5nni  7698  nnre  7702  nncn  7703  nnind  7711  nnnn0  7964  nn0re  7966  nn0cn  7967  nnz  8040  nn0z  8041  nnq  8344  qcn  8345  rpre  8364  iccshftri  8633  iccshftli  8635  iccdili  8637  icccntri  8639  fzval2  8647  fzelp1  8706  4fvwrd4  8767  elfzo1  8816  expcllem  8920  expcl2lemap  8921  m1expcl2  8931
  Copyright terms: Public domain W3C validator