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

Theorem sseldd 3102
Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
sseldd.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
sseldd  |-  ( ph  ->  C  e.  B )

Proof of Theorem sseldd
StepHypRef Expression
1 sseldd.2 . 2  |-  ( ph  ->  C  e.  A )
2 sseld.1 . . 3  |-  ( ph  ->  A  C_  B )
32sseld 3100 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
41, 3mpd 13 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:  disjiun  3931  exmid01  4128  frirrg  4279  ordtri2or2exmid  4493  riotass  5764  tfrcldm  6267  nntr2  6406  eroveu  6527  eroprf  6529  ixpssmapg  6629  findcard2d  6792  findcard2sd  6793  fimax2gtrilemstep  6801  undifdc  6819  fisseneq  6827  fidcenumlemrks  6848  fidcenumlemr  6850  fiuni  6873  suplub2ti  6895  ctssdclemn0  7002  acfun  7079  ccfunen  7095  nnppipi  7174  archnqq  7248  prarloclemlt  7324  suplocexprlemrl  7548  suplocexprlemmu  7549  suplocexprlemdisj  7551  suplocexprlemloc  7552  suplocexprlemex  7553  suplocexprlemub  7554  suplocexprlemlub  7555  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  axpre-suploclemres  7732  suprubex  8732  suprzclex  9172  fzssp1  9877  elfzoelz  9954  fzofzp1  10034  fzostep1  10044  frecuzrdgg  10219  frecuzrdgdomlem  10220  frecuzrdgsuctlem  10226  ser3mono  10281  bcm1k  10537  fimaxq  10604  leisorel  10611  zfz1isolemiso  10613  seq3coll  10616  fimaxre2  11029  summodclem2a  11181  fsum3cvg3  11196  fsumcl2lem  11198  fsum0diaglem  11240  fsumiun  11277  prodmodclem2a  11376  zssinfcl  11675  ennnfonelemhom  11962  exmidunben  11973  ctiunctlemfo  11986  strsetsid  12029  strslssd  12042  topssnei  12368  cnprcl2k  12412  cnss1  12432  cnptopresti  12444  cnptoprest  12445  lmres  12454  txopn  12471  txcnp  12477  xmetres2  12585  blin2  12638  blopn  12696  xmettxlem  12715  xmettx  12716  elcncf2  12767  cncfmet  12785  cncfmptc  12788  cncfmptid  12789  negcncf  12794  mulcncflem  12796  cnrehmeocntop  12799  dedekindeulemuub  12801  dedekindeulemlu  12805  suplociccreex  12808  suplociccex  12809  dedekindicclemuub  12810  dedekindicclemlu  12814  dedekindicclemeu  12815  dedekindicclemicc  12816  ivthinclemlopn  12820  ivthinclemuopn  12822  ivthdec  12828  limcimolemlt  12839  cnplimcim  12842  cnplimclemle  12843  cnplimclemr  12844  cnlimci  12848  limccnpcntop  12850  limccnp2lem  12851  limccnp2cntop  12852  dvlemap  12855  dvfgg  12863  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvcjbr  12878  reeff1olem  12898  sssneq  13368
  Copyright terms: Public domain W3C validator