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

Theorem sseld 3038
Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
sseld.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
sseld (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem sseld
StepHypRef Expression
1 sseld.1 . 2 (𝜑𝐴𝐵)
2 ssel 3033 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1445  wss 3013
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026
This theorem is referenced by:  sselda  3039  sseldd  3040  ssneld  3041  elelpwi  3461  ssbrd  3908  uniopel  4107  onintonm  4362  sucprcreg  4393  ordsuc  4407  0elnn  4460  dmrnssfld  4728  nfunv  5081  opelf  5217  fvimacnv  5453  ffvelrn  5471  resflem  5501  f1imass  5591  dftpos3  6065  nnmordi  6315  mapsn  6487  ixpf  6517  diffifi  6690  ordiso2  6808  prarloclemarch2  7075  ltexprlemrl  7266  cauappcvgprlemladdrl  7313  caucvgprlemladdrl  7334  caucvgprlem1  7335  uzind  8956  supinfneg  9182  infsupneg  9183  ixxssxr  9466  elfz0add  9683  fzoss1  9731  frecuzrdgrclt  9971  fsum3cvg  10936  isumrpcl  11053  lmtopcnp  12117  xmetunirn  12160  mopnval  12244  metrest  12308  bj-nnord  12577
  Copyright terms: Public domain W3C validator