MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseldd Structured version   Unicode version

Theorem sseldd 3349
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 3347 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
41, 3mpd 15 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    C_ wss 3320
This theorem is referenced by:  ordunel  4807  sofld  5318  soisores  6047  riotass  6578  tfrlem13  6651  omordi  6809  oeeulem  6844  oeeui  6845  uniinqs  6984  eroveu  6999  eroprf  7002  ixpssmapg  7092  omxpenlem  7209  nnunifi  7358  unifpw  7409  dffi3  7436  ordtypelem6  7492  oismo  7509  unxpwdom2  7556  cantnfval2  7624  cantnfle  7626  cantnflt  7627  cantnfp1lem3  7636  cantnflem1b  7642  cantnflem1d  7644  cantnflem1  7645  cantnflem4  7648  cnfcomlem  7656  cnfcom  7657  cnfcom3lem  7660  cnfcom3  7661  cnfcom3clem  7662  r1sscl  7711  tz9.12lem3  7715  pwwf  7733  rankonidlem  7754  r1pw  7771  r0weon  7894  dfac8clem  7913  iunfictbso  7995  dfac12lem2  8024  infpssrlem3  8185  ssfin4  8190  fin23lem11  8197  fin23lem24  8202  fin23lem26  8205  fin23lem23  8206  fin23lem22  8207  fin23lem27  8208  fin1a2lem9  8288  fin1a2lem11  8290  hsmexlem3  8308  ttukeylem6  8394  ttukeylem7  8395  iunfo  8414  fpwwe2lem6  8510  fpwwe2lem9  8513  fpwwe2lem12  8516  pwfseqlem5  8538  gch2  8554  wunss  8587  wunf  8602  r1limwun  8611  wunex2  8613  inttsk  8649  tskuni  8658  wloglei  9559  suprzcl  10349  suprzub  10567  uzwo3  10569  rpnnen1lem5  10604  fzssp1  11095  elfzoelz  11140  fzofzp1  11189  fzostep1  11197  fseqsupcl  11316  sermono  11355  seqf1olem2a  11361  seqf1olem2  11363  bcm1k  11606  seqcoll  11712  seqcoll2  11713  swrdcl  11766  splfv1  11784  splfv2a  11785  rlimclim1  12339  rlimresb  12359  rlimcld2  12372  o1rlimmul  12412  lo1le  12445  isercolllem2  12459  caucvgrlem  12466  summolem2a  12509  fsumcvg3  12523  fsumcl2lem  12525  fsum0diaglem  12560  mertenslem2  12662  bitsfzolem  12946  bitsfzo  12947  vdwlem1  13349  vdwlem2  13350  vdwlem5  13353  vdwlem6  13354  vdwlem8  13356  vdwlem9  13357  vdwlem11  13359  0ram  13388  0ramcl  13391  ramub1lem1  13394  strssd  13503  imasvscafn  13762  mrieqvlemd  13854  mrieqv2d  13864  mreexexlem2d  13870  isacs2  13878  ssctr  14025  ssceq  14026  subcss2  14040  subccatid  14043  fullresc  14048  funcres  14093  ffthiso  14126  rescfth  14134  ressffth  14135  resssetc  14247  funcsetcres2  14248  resscatc  14260  catcisolem  14261  catciso  14262  yonedalem1  14369  yonffthlem  14379  yoniso  14382  lubun  14550  ipodrsima  14591  isacs3lem  14592  acsmapd  14604  resmhm  14759  mhmima  14763  gsumress  14777  gsumval2  14783  gsumwspan  14791  frmdss2  14808  mulgnnsubcl  14902  mulgnn0subcl  14903  mulgsubcl  14904  mulgpropd  14923  submmulg  14925  subg0  14950  subgsubcl  14955  subgsub  14956  subgmulg  14958  issubg4  14961  nsgconj  14973  ssnmz  14982  ghmnsgima  15029  subgga  15077  gasubg  15079  cntzrcl  15126  cntrsubgnsg  15139  odf1o1  15206  odcau  15238  sylow2blem1  15254  sylow2blem2  15255  sylow2blem3  15256  sylow3lem2  15262  lsmub1x  15280  lsmsubm  15287  lsmsubg  15288  lsmass  15302  lsmmod  15307  lsmpropd  15309  lsmdisj2  15314  subgdisj1  15323  subgdisj2  15324  pj1id  15331  pj1ghm  15335  efgsp1  15369  efgsres  15370  efgsfo  15371  efgredlemf  15373  efgredlemd  15376  subgabl  15455  lsmcomx  15471  gsumzadd  15527  gsumzsplit  15529  dprdfcntz  15573  dprdfadd  15578  dprdfeq0  15580  dprdlub  15584  dprdres  15586  dprd2dlem2  15598  dprd2da  15600  dmdprdsplit2lem  15603  dpjrid  15620  ablfac1b  15628  ablfac1eulem  15630  pgpfac1lem1  15632  pgpfac1lem2  15633  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfac1lem4  15636  pgpfac1lem5  15637  isdrng2  15845  subrguss  15883  subrginv  15884  subrgdv  15885  issubdrg  15893  abvres  15927  islss3  16035  lspsnel3  16067  lsspropd  16093  reslmhm  16128  lbspss  16154  lsmsp  16158  lspprabs  16167  pj1lmhm  16172  pj1lmhm2  16173  lspindpi  16204  lvecindp  16210  lsmcv  16213  lspsolvlem  16214  lspsolv  16215  lspsnat  16217  lsppratlem1  16219  lsppratlem3  16221  lsppratlem4  16222  islbs2  16226  lbsextlem2  16231  lbsextlem3  16232  domnrrg  16360  issubassa  16383  sraassa  16384  issubassa2  16403  resspsradd  16479  resspsrmul  16480  resspsrvsca  16481  mplbas2  16531  mplind  16562  qsssubdrg  16758  cnsubrg  16759  zlpirlem3  16770  lsmcss  16919  cssmre  16920  pjdm2  16938  pjf2  16941  pjfo  16942  ocvpj  16944  obselocv  16955  toponmre  17157  topssnei  17188  neiptopuni  17194  neiptoptop  17195  neiptopnei  17196  ordtbas2  17255  ordtopn1  17258  ordtopn2  17259  cnss1  17340  cnprest  17353  lmres  17364  iuncon  17491  concompcld  17497  concompclo  17498  2ndcctbss  17518  2ndcdisj  17519  dis2ndc  17523  llycmpkgen2  17582  1stckgenlem  17585  kgen2cn  17591  ptbasfi  17613  ptopn  17615  txopn  17634  ptpjcn  17643  ptpjopn  17644  txcnp  17652  ptrescn  17671  txtube  17672  xkopjcn  17688  kqreglem2  17774  reghmph  17825  isufil2  17940  ssufl  17950  ufileu  17951  filufint  17952  fmfnfmlem2  17987  fmfnfmlem4  17989  fmfnfm  17990  flimfil  18001  flimcf  18014  flimclslem  18016  hauspwpwf1  18019  fclscf  18057  fclsfnflim  18059  flimfnfcls  18060  cnpfcfi  18072  cnpfcf  18073  alexsublem  18075  alexsubALTlem3  18080  alexsubALTlem4  18081  cnextfun  18095  cnextcn  18098  subgntr  18136  tsmsmhm  18175  tsmsadd  18176  tsmssub  18178  tgptsmscls  18179  tsmsxp  18184  invrcn  18210  ustelimasn  18252  utoptop  18264  restutopopn  18268  utop3cls  18281  utopreg  18282  ucncn  18315  cfilufg  18323  xmetres2  18391  prdsmet  18400  ressprdsds  18401  blin2  18459  blopn  18530  lpbl  18533  met2ndci  18552  prdsxmslem2  18559  metustssOLD  18583  metustss  18584  metustexhalfOLD  18593  metustexhalf  18594  metustOLD  18597  metust  18598  metutopOLD  18612  psmetutop  18613  subgngp  18676  sranlm  18720  lssnlm  18736  icccmplem1  18853  icccmplem2  18854  icccmplem3  18855  reconnlem1  18857  reconnlem2  18858  reconn  18859  xrge0gsumle  18864  xrge0tsms  18865  metnrmlem1a  18888  metnrmlem1  18889  elcncf2  18920  cncfmet  18938  cncfmptid  18942  cnmpt2pc  18953  icccvx  18975  cnrehmeo  18978  cnheiborlem  18979  cnheibor  18980  cnllycmp  18981  bndth  18983  lebnumlem1  18986  lebnum  18989  htpycom  19001  htpyco1  19003  htpyco2  19004  htpycc  19005  phtpy01  19010  phtpycom  19013  phtpyco2  19015  phtpycc  19016  reparphti  19022  pcohtpylem  19044  clmvneg1  19116  clmmulg  19118  nmoleub3  19127  cphsubrglem  19140  cphreccllem  19141  cphdivcl  19145  cphsqrcl2  19149  cphsqrcl3  19150  cphipcl  19154  cphassr  19174  cph2ass  19175  tchcphlem3  19190  ipcau2  19191  tchcphlem1  19192  tchcphlem2  19193  tchcph  19194  nmparlem  19196  iscfil3  19226  caublcls  19261  cmetss  19267  bcthlem3  19279  bcthlem4  19280  bcthlem5  19281  minveclem2  19327  minveclem3  19330  minveclem4a  19331  minveclem4b  19332  minveclem4  19333  minveclem7  19336  pjthlem1  19338  pjthlem2  19339  cldcss  19342  pmltpclem2  19346  ivthlem2  19349  ivthlem3  19350  ivth2  19352  ivthicc  19355  ovolctb  19386  ovolunlem1a  19392  ovolicc2lem4  19416  ovolicc2lem5  19417  ioombl1lem2  19453  ioombl1lem4  19455  dyadmaxlem  19489  dyadmbllem  19491  vitalilem2  19501  vitalilem3  19502  itg1val2  19576  itg1addlem1  19584  i1fmullem  19586  i1fadd  19587  limccl  19762  limcflflem  19767  limcflf  19768  limcmpt2  19771  cnplimc  19774  cnlimci  19776  limccnp2  19779  dvlem  19783  dvres2lem  19797  dvcnp2  19806  dvnadd  19815  cpncn  19822  dvaddbr  19824  dvmulbr  19825  dvcmul  19830  dvcobr  19832  dvcjbr  19835  dvcnvlem  19860  dvferm1lem  19868  dvferm1  19869  dvferm2lem  19870  dvferm2  19871  dvlip  19877  dvlipcn  19878  c1liplem1  19880  c1lip1  19881  dv11cn  19885  dvgt0lem1  19886  dvgt0  19888  dvlt0  19889  dvge0  19890  dvivthlem1  19892  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop1  19898  lhop  19900  dvcnvrelem1  19901  dvcnvrelem2  19902  dvcnvre  19903  dvcvx  19904  ftc1lem1  19919  ftc1a  19921  ftc1lem4  19923  ftc1lem5  19924  ftc1lem6  19925  ftc1  19926  ftc2ditglem  19929  ftc2ditg  19930  mpff  19962  mpfaddcl  19963  mpfmulcl  19964  pf1f  19970  mdegcl  19992  deg1invg  20029  ply1divalg  20060  uc1pmon1p  20074  fta1glem1  20088  ig1peu  20094  ig1pdvds  20099  ig1prsp  20100  ply1lpir  20101  plyf  20117  plyeq0lem  20129  plypf1  20131  plyco  20160  dvply2g  20202  plydivlem4  20213  aannenlem2  20246  taylfvallem1  20273  tayl0  20278  taylplem1  20279  taylply2  20284  taylply  20285  dvtaylp  20286  taylthlem1  20289  taylthlem2  20290  ulmdvlem1  20316  ulmdvlem3  20318  pserulm  20338  pserdv  20345  abelthlem6  20352  abelthlem7  20354  efif1olem4  20447  eff1olem  20450  logccv  20554  rlimcnp  20804  xrlimcnp  20807  cvxcl  20823  scvxcvx  20824  jensenlem2  20826  jensen  20827  wilthlem2  20852  lgsquadlem3  21140  dchrisumlem2  21184  pntpbnd1  21280  pntibndlem2  21285  pntlem3  21303  umgraex  21358  subgoid  21895  subgoinv  21896  sspz  22234  ubthlem2  22373  minvecolem2  22377  minvecolem3  22378  minvecolem4b  22380  minvecolem7  22385  occllem  22805  pjhcl  22903  pjpjpre  22921  chscllem2  23140  chscllem3  23141  chscllem4  23142  shatomistici  23864  sumdmdlem2  23922  elovimad  24051  opfv  24058  xrofsup  24126  ssnnssfz  24148  toslub  24191  tosglb  24192  gsumpropd2lem  24220  xrge0tsmsd  24223  subofld  24245  metideq  24288  xpinpreima2  24305  tpr2rico  24310  lmxrge0  24337  lmdvg  24338  ind1  24416  esumcl  24427  gsumesum  24451  esumlub  24452  esumfsup  24460  esumpcvgval  24468  esumpmono  24469  esumcvg  24476  elsigagen2  24531  elsx  24548  measinb  24575  volmeas  24587  imambfm  24612  cnmbfm  24613  sibfof  24654  orvcoel  24719  orvccel  24720  ballotlemsdom  24769  ballotlemfrceq  24786  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem5  24817  lgamgulmlem6  24818  lgamucov  24822  erdsze2lem2  24890  conpcon  24922  txsconlem  24927  cvxpcon  24929  cvxscon  24930  cnllyscon  24932  rescon  24933  cvmsf1o  24959  cvmfolem  24966  cvmliftmolem1  24968  cvmliftmolem2  24969  cvmliftlem3  24974  cvmliftlem6  24977  cvmliftlem7  24978  cvmliftlem8  24979  cvmlift2lem9a  24990  cvmlift2lem9  24998  cvmlift2lem11  25000  cvmlift2lem12  25001  cvmliftphtlem  25004  cvmlift3lem6  25011  cvmlift3lem7  25012  prodmolem2a  25260  fprodcl2lem  25276  nodenselem3  25638  axlowdimlem17  25897  axcontlem4  25906  axcontlem9  25911  axcontlem10  25912  linethru  26087  cnambfre  26255  ftc1cnnclem  26278  ftc1cnnc  26279  ivthALT  26338  comppfsc  26387  neibastop1  26388  neibastop2lem  26389  filnetlem3  26409  sdclem2  26446  caures  26466  sstotbnd2  26483  ssbnd  26497  totbndbnd  26498  prdsbnd  26502  prdstotbnd  26503  prdsbnd2  26504  heiborlem3  26522  heiborlem5  26524  heiborlem6  26525  heiborlem8  26527  reheibor  26548  istopclsd  26754  isnacs3  26764  diophrw  26817  rencldnfilem  26881  pellfundglb  26948  pellfundex  26949  pellfund14  26961  pellfund14b  26962  rmspecfund  26972  rmxyelqirr  26973  setindtr  27095  aomclem2  27130  kelac2  27140  frlmplusgval  27206  frlmvscafval  27207  frlmssuvc1  27223  frlmsslsp  27225  isnumbasgrplem2  27246  lindff1  27267  hbtlem2  27305  hbtlem4  27307  hbtlem5  27309  cnsrexpcl  27347  cnsrplycl  27349  rngunsnply  27355  pmtrf  27374  pmtrfinv  27379  symggen  27388  psgnunilem1  27393  psgnunilem5  27394  mon1psubm  27502  ubelsupr  27667  cncmpmax  27679  climinf  27708  climsuse  27710  stoweidlem7  27732  stoweidlem11  27736  stoweidlem26  27751  stoweidlem29  27754  stoweidlem31  27756  stoweidlem34  27759  stoweidlem36  27761  stoweidlem46  27771  stoweidlem52  27777  stoweidlem53  27778  stoweid  27788  iunconlem2  29047  bnj907  29336  bnj1121  29354  bnj1128  29359  bnj1175  29373  bnj1177  29375  bnj1417  29410  lubunNEW  29771  lshpnel  29781  lshpnelb  29782  lsatlssel  29795  lsmsat  29806  lssats  29810  lrelat  29812  lsmcv2  29827  lcvexchlem1  29832  lcvexchlem2  29833  lcvexchlem3  29834  lcvexchlem4  29835  lcvexchlem5  29836  lcv1  29839  lcv2  29840  lsatexch  29841  lsatcv0eq  29845  lsatcvatlem  29847  lsatcvat  29848  lsatcvat3  29850  l1cvat  29853  lkrlsp  29900  lshpsmreu  29907  lshpkrlem5  29912  paddcom  30610  paddasslem11  30627  paddasslem12  30628  paddasslem13  30629  pmodlem1  30643  pclfinN  30697  osumcllem6N  30758  osumcllem9N  30761  osumcllem11N  30763  pexmidlem3N  30769  dia2dimlem5  31866  dia2dimlem9  31870  dvhopellsm  31915  diblss  31968  diblsmopel  31969  dicvaddcl  31988  dicvscacl  31989  cdlemn5pre  31998  cdlemn11b  32006  cdlemn11c  32007  dihjustlem  32014  dihord1  32016  dihord2a  32017  dihord2b  32018  dihord11b  32020  dihord11c  32022  dihopcl  32051  dihord6apre  32054  dihord5b  32057  dihord5apre  32060  dihglblem2aN  32091  dihglblem2N  32092  dihglblem3N  32093  dihglblem4  32095  dihglblem5  32096  dihglbcpreN  32098  dihjatc3  32111  dihmeetlem9N  32113  dihjatcclem1  32216  dihjatcclem2  32217  dihjat  32221  dvh3dim3N  32247  dochexmidlem2  32259  dochexmidlem6  32263  dochexmidlem7  32264  dochsnkr  32270  dochfln0  32275  lcfl6lem  32296  lcfl6  32298  lclkrlem2b  32306  lclkrlem2f  32310  lclkrlem2v  32326  lclkrslem2  32336  lcfrlem4  32343  lcfrlem16  32356  lcfrlem23  32363  lcfrlem25  32365  lcfrlem31  32371  lcfrlem33  32373  lcfrlem35  32375  lcdvbaselfl  32393  mapdrvallem2  32443  mapdlsm  32462  mapdpglem3  32473  mapdpglem9  32478  mapdpglem14  32483  mapdpglem17N  32486  mapdpglem18  32487  mapdpglem21  32490  mapdindp0  32517  lspindp5  32568  hdmaprnlem4tN  32653  hdmaprnlem4N  32654  hdmaprnlem3eN  32659  hdmapinvlem1  32719  hdmapinvlem2  32720  hdmapinvlem3  32721  hdmapinvlem4  32722  hdmapglem5  32723  hdmapglem7a  32728  hdmapglem7b  32729  hdmapglem7  32730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator