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

Theorem sseld 2972
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 2967 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  sselda  2973  sseldd  2974  ssneld  2975  elelpwi  3398  ssbrd  3833  uniopel  4021  onintonm  4271  sucprcreg  4301  ordsuc  4315  0elnn  4368  dmrnssfld  4623  nfunv  4961  opelf  5090  fvimacnv  5310  ffvelrn  5328  f1imass  5441  dftpos3  5908  nnmordi  6120  diffifi  6382  ordiso2  6415  prarloclemarch2  6575  ltexprlemrl  6766  cauappcvgprlemladdrl  6813  caucvgprlemladdrl  6834  caucvgprlem1  6835  uzind  8408  ixxssxr  8870  elfz0add  9081  elfz0addOLD  9082  fzoss1  9129  iseqss  9390  bj-nnord  10470
  Copyright terms: Public domain W3C validator