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

Theorem sseld 3064
Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
sseld  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )

Proof of Theorem sseld
StepHypRef Expression
1 sseld.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssel 3059 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463    C_ wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  sselda  3065  sseldd  3066  ssneld  3067  elelpwi  3490  ssbrd  3939  uniopel  4146  onintonm  4401  sucprcreg  4432  ordsuc  4446  0elnn  4500  dmrnssfld  4770  nfunv  5124  opelf  5262  fvimacnv  5501  ffvelrn  5519  resflem  5550  f1imass  5641  dftpos3  6125  nnmordi  6378  mapsn  6550  ixpf  6580  diffifi  6754  ordiso2  6886  difinfinf  6952  prarloclemarch2  7191  ltexprlemrl  7382  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  caucvgprlem1  7451  axpre-suploclemres  7673  uzind  9116  supinfneg  9342  infsupneg  9343  ixxssxr  9634  elfz0add  9851  fzoss1  9899  frecuzrdgrclt  10139  fsum3cvg  11097  isumrpcl  11214  lmtopcnp  12325  txuni2  12331  tx1cn  12344  tx2cn  12345  txlm  12354  imasnopn  12374  xmetunirn  12433  mopnval  12517  metrest  12581  dedekindicc  12686  ivthdec  12697  limcimolemlt  12708  bj-nnord  12990
  Copyright terms: Public domain W3C validator