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

Theorem sseli 2914
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 2912 . 2 (AB → (𝐶 A𝐶 B))
31, 2ax-mp 7 1 (𝐶 A𝐶 B)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1370  wss 2890
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 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-in 2897  df-ss 2904
This theorem is referenced by:  sselii  2915  sseldi  2916  elun1  3083  elun2  3084  finds  4246  finds2  4247  issref  4630  2elresin  4932  fvun1  5160  fvmptssdm  5176  fvimacnvi  5202  elpreima  5207  ofrfval  5639  fnofval  5640  off  5643  offres  5681  eqopi  5717  op1steq  5724  dfoprab4  5737  reldmtpos  5786  smores3  5826  smores2  5827  pinn  6163  enq0enq  6280  preqlu  6320  elinp  6322  prop  6323  elnp1st2nd  6324  prarloclem5  6348  recn  6623  rexr  6679
  Copyright terms: Public domain W3C validator