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

Theorem sseli 3063
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 3061 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  sselii  3064  sseldi  3065  elun1  3213  elun2  3214  finds  4484  finds2  4485  issref  4891  2elresin  5204  fvun1  5455  fvmptssdm  5473  elfvmptrab1  5483  fvimacnvi  5502  elpreima  5507  ofrfval  5958  ofvalg  5959  off  5962  offres  6001  eqopi  6038  op1steq  6045  dfoprab4  6058  f1od2  6100  reldmtpos  6118  smores3  6158  smores2  6159  ctssdccl  6964  pinn  7085  indpi  7118  enq0enq  7207  preqlu  7248  elinp  7250  prop  7251  elnp1st2nd  7252  prarloclem5  7276  cauappcvgprlemladd  7434  peano5nnnn  7668  nnindnn  7669  recn  7721  rexr  7779  peano5nni  8691  nnre  8695  nncn  8696  nnind  8704  nnnn0  8952  nn0re  8954  nn0cn  8955  nn0xnn0  9012  nnz  9041  nn0z  9042  nnq  9393  qcn  9394  rpre  9416  iccshftri  9746  iccshftli  9748  iccdili  9750  icccntri  9752  fzval2  9761  fzelp1  9822  4fvwrd4  9885  elfzo1  9935  expcllem  10272  expcl2lemap  10273  m1expcl2  10283  bcm1k  10474  bcpasc  10480  cau3lem  10854  climconst2  11028  fsum3  11124  binomlem  11220  cos12dec  11401  dvdsflip  11476  infssuzcldc  11571  isprm3  11726  phimullem  11828  structcnvcnv  11902  fvsetsid  11920  tgval2  12147  qtopbasss  12617  dedekindicc  12707  ivthinc  12717  ivthdec  12718  cosz12  12788  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator