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

Theorem sseldi 3021
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
Hypotheses
Ref Expression
sseli.1 𝐴𝐵
sseldi.2 (𝜑𝐶𝐴)
Assertion
Ref Expression
sseldi (𝜑𝐶𝐵)

Proof of Theorem sseldi
StepHypRef Expression
1 sseldi.2 . 2 (𝜑𝐶𝐴)
2 sseli.1 . . 3 𝐴𝐵
32sseli 3019 . 2 (𝐶𝐴𝐶𝐵)
41, 3syl 14 1 (𝜑𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1438  wss 2997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010
This theorem is referenced by:  riotacl  5604  riotasbc  5605  elmpt2cl  5824  ofrval  5848  f1od2  5982  mpt2xopn0yelv  5986  tpostpos  6011  smores  6039  supubti  6673  suplubti  6674  prarloclemcalc  7040  rereceu  7403  recriota  7404  rexrd  7516  nnred  8407  nncnd  8408  un0addcl  8676  un0mulcl  8677  nnnn0d  8696  nn0red  8697  nn0xnn0d  8715  suprzclex  8814  nn0zd  8836  zred  8838  rpred  9142  ige2m1fz  9491  zmodfzp1  9720  iseqcaopr2  9876  expcl2lemap  9932  m1expcl  9943  isummolem2a  10735  zisum  10738  lcmn0cl  11132
  Copyright terms: Public domain W3C validator