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

Theorem sseldi 3099
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
Hypotheses
Ref Expression
sseli.1  |-  A  C_  B
sseldi.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
sseldi  |-  ( ph  ->  C  e.  B )

Proof of Theorem sseldi
StepHypRef Expression
1 sseldi.2 . 2  |-  ( ph  ->  C  e.  A )
2 sseli.1 . . 3  |-  A  C_  B
32sseli 3097 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3syl 14 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481    C_ wss 3075
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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3081  df-ss 3088
This theorem is referenced by:  mptrcl  5510  riotacl  5751  riotasbc  5752  elmpocl  5975  ofrval  5999  f1od2  6139  mpoxopn0yelv  6143  tpostpos  6168  smores  6196  supubti  6893  suplubti  6894  prarloclemcalc  7333  rereceu  7720  recriota  7721  rexrd  7838  eqord1  8268  nnred  8756  nncnd  8757  un0addcl  9033  un0mulcl  9034  nnnn0d  9053  nn0red  9054  nn0xnn0d  9072  suprzclex  9172  nn0zd  9194  zred  9196  rpred  9512  ige2m1fz  9920  zmodfzp1  10151  seq3caopr2  10285  expcl2lemap  10335  m1expcl  10346  summodclem2a  11181  zsumdc  11184  clim2prod  11339  ntrivcvgap  11348  prodmodclem2a  11376  zproddc  11379  lcmn0cl  11783  ennnfonelemg  11950  lmrcl  12397  lmss  12452  upxp  12478  isxms2  12658  iooretopg  12734  tgqioo  12753  limccoap  12853  dvcl  12858  dvidlemap  12866  dvcnp2cntop  12869  isomninnlem  13398  trilpolemeq1  13406  trilpolemlt1  13407  iswomninnlem  13415  ismkvnnlem  13417
  Copyright terms: Public domain W3C validator