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

Theorem sseldd 3352
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 3350 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
41, 3mpd 15 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sofld  5281  soisores  6013  riotass  6075  ovima0  6237  ordunel  6433  tfrlem13  6841  omordi  6997  oeeulem  7032  oeeui  7033  uniinqs  7172  eroveu  7187  eroprf  7190  ixpssmapg  7285  omxpenlem  7404  findcard2d  7546  nnunifi  7555  unifpw  7606  dffi3  7673  ordtypelem6  7729  oismo  7746  unxpwdom2  7795  cantnfval2  7869  cantnfle  7871  cantnflt  7872  cantnfres  7877  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnflem4  7892  cantnfval2OLD  7899  cantnfleOLD  7901  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnflem4OLD  7914  cnfcomlem  7924  cnfcom  7925  cnfcom3lem  7928  cnfcom3  7929  cnfcom3clem  7930  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom3lemOLD  7936  cnfcom3OLD  7937  cnfcom3clemOLD  7938  r1sscl  7984  tz9.12lem3  7988  pwwf  8006  rankonidlem  8027  r1pw  8044  r0weon  8171  dfac8clem  8194  iunfictbso  8276  dfac12lem2  8305  infpssrlem3  8466  ssfin4  8471  fin23lem11  8478  fin23lem24  8483  fin23lem26  8486  fin23lem23  8487  fin23lem22  8488  fin23lem27  8489  fin1a2lem9  8569  fin1a2lem11  8571  hsmexlem3  8589  ttukeylem6  8675  ttukeylem7  8676  iunfo  8695  fpwwe2lem6  8794  fpwwe2lem9  8797  fpwwe2lem12  8800  pwfseqlem5  8822  gch2  8834  wunss  8871  wunf  8886  r1limwun  8895  wunex2  8897  inttsk  8933  tskuni  8942  wloglei  9864  suprzcl  10713  suprzub  10938  uzwo3  10940  rpnnen1lem5  10975  supicclub  11427  supicclub2  11428  fzssp1  11493  elfzoelz  11545  fzofzp1  11616  fzostep1  11627  fseqsupcl  11791  sermono  11830  seqf1olem2a  11836  seqf1olem2  11838  bcm1k  12083  seqcoll  12208  seqcoll2  12209  swrdcl  12307  splfv1  12389  splfv2a  12390  rlimclim1  13015  rlimresb  13035  rlimcld2  13048  o1rlimmul  13088  lo1le  13121  isercolllem2  13135  caucvgrlem  13142  summolem2a  13184  fsumcvg3  13198  fsumcl2lem  13200  fsum0diaglem  13235  mertenslem2  13337  bitsfzolem  13622  bitsfzo  13623  vdwlem1  14034  vdwlem2  14035  vdwlem5  14038  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  vdwlem11  14044  0ram  14073  0ramcl  14076  ramub1lem1  14079  strssd  14202  imasvscafn  14467  mrieqvlemd  14559  mrieqv2d  14569  mreexexlem2d  14575  isacs2  14583  ssctr  14730  ssceq  14731  subcss2  14745  subccatid  14748  fullresc  14753  funcres  14798  ffthiso  14831  rescfth  14839  ressffth  14840  resssetc  14952  funcsetcres2  14953  resscatc  14965  catcisolem  14966  catciso  14967  yonedalem1  15074  yonffthlem  15084  yoniso  15087  lubun  15285  ipodrsima  15327  isacs3lem  15328  acsmapd  15340  resmhm  15478  mhmima  15482  mrcmndind  15485  gsumpropd2lem  15496  gsumress  15498  gsumval2  15504  gsumwspan  15515  frmdss2  15532  grpidssd  15593  grpinvssd  15594  mulgnnsubcl  15630  mulgnn0subcl  15631  mulgsubcl  15632  mulgpropd  15651  submmulg  15653  subg0  15678  subgsubcl  15683  subgsub  15684  subgmulg  15686  issubg4  15691  nsgconj  15705  ssnmz  15714  ghmnsgima  15761  subgga  15809  gasubg  15811  cntzrcl  15836  cntrsubgnsg  15849  pmtrf  15952  pmtrfinv  15958  symggen  15967  psgnunilem1  15990  psgnunilem5  15991  odf1o1  16062  odcau  16094  sylow2blem1  16110  sylow2blem2  16111  sylow2blem3  16112  sylow3lem2  16118  lsmub1x  16136  lsmsubm  16143  lsmsubg  16144  lsmass  16158  lsmmod  16163  lsmpropd  16165  lsmdisj2  16170  subgdisj1  16179  subgdisj2  16180  pj1id  16187  pj1ghm  16191  efgsp1  16225  efgsres  16226  efgsfo  16227  efgredlemf  16229  efgredlemd  16232  subgabl  16311  lsmcomx  16329  gsumzadd  16400  gsumzaddOLD  16402  gsumzsplit  16409  gsumzsplitOLD  16410  dprdfcntz  16487  dprdfcntzOLD  16493  dprdfadd  16498  dprdfeq0  16500  dprdfaddOLD  16505  dprdfeq0OLD  16507  dprdlub  16511  dprdres  16513  dprd2dlem2  16527  dprd2da  16529  dmdprdsplit2lem  16532  dpjrid  16549  ablfac1b  16559  ablfac1eulem  16561  pgpfac1lem1  16563  pgpfac1lem2  16564  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfac1lem4  16567  pgpfac1lem5  16568  isdrng2  16820  subrguss  16858  subrginv  16859  subrgdv  16860  issubdrg  16868  abvres  16902  islss3  17017  lspsnel3  17049  lsspropd  17075  reslmhm  17110  lbspss  17140  lsmsp  17144  lspprabs  17153  pj1lmhm  17158  pj1lmhm2  17159  lspindpi  17190  lvecindp  17196  lsmcv  17199  lspsolvlem  17200  lspsolv  17201  lspsnat  17203  lsppratlem1  17205  lsppratlem3  17207  lsppratlem4  17208  islbs2  17212  lbsextlem2  17217  lbsextlem3  17218  domnrrg  17349  issubassa  17372  sraassa  17373  issubassa2  17392  resspsradd  17465  resspsrmul  17466  resspsrvsca  17467  mplbas2  17526  mplbas2OLD  17527  mplind  17559  evlsscasrng  17587  mpff  17594  mpfaddcl  17595  mpfmulcl  17596  evls1sca  17733  evls1scasrng  17748  pf1f  17759  qsssubdrg  17847  cnsubrg  17848  zringlpirlem3  17880  zlpirlem3  17885  lsmcss  18092  cssmre  18093  pjdm2  18111  pjf2  18114  pjfo  18115  ocvpj  18117  obselocv  18128  frlmplusgval  18166  frlmvscafval  18168  frlmssuvc1  18194  frlmssuvc1OLD  18196  frlmsslsp  18198  frlmsslspOLD  18199  lindff1  18224  mdetrlin2  18388  mdetunilem5  18397  toponmre  18672  topssnei  18703  neiptopuni  18709  neiptoptop  18710  neiptopnei  18711  ordtbas2  18770  ordtopn1  18773  ordtopn2  18774  cnss1  18855  cnprest  18868  lmres  18879  iuncon  19007  concompcld  19013  concompclo  19014  2ndcctbss  19034  2ndcdisj  19035  dis2ndc  19039  llycmpkgen2  19098  1stckgenlem  19101  kgen2cn  19107  ptbasfi  19129  ptopn  19131  txopn  19150  ptpjcn  19159  ptpjopn  19160  txcnp  19168  ptrescn  19187  txtube  19188  xkopjcn  19204  kqreglem2  19290  reghmph  19341  isufil2  19456  ssufl  19466  ufileu  19467  filufint  19468  fmfnfmlem2  19503  fmfnfmlem4  19505  fmfnfm  19506  flimfil  19517  flimcf  19530  flimclslem  19532  hauspwpwf1  19535  fclscf  19573  fclsfnflim  19575  flimfnfcls  19576  cnpfcfi  19588  cnpfcf  19589  alexsublem  19591  alexsubALTlem3  19596  alexsubALTlem4  19597  cnextfun  19611  cnextcn  19614  subgntr  19652  tsmsmhm  19695  tsmsadd  19696  tsmssub  19698  tgptsmscls  19699  tsmsxp  19704  invrcn  19730  ustelimasn  19772  utoptop  19784  restutopopn  19788  utop3cls  19801  utopreg  19802  ucncn  19835  cfilufg  19843  xmetres2  19911  prdsmet  19920  ressprdsds  19921  blin2  19979  blopn  20050  lpbl  20053  met2ndci  20072  prdsxmslem2  20079  metustssOLD  20103  metustss  20104  metustexhalfOLD  20113  metustexhalf  20114  metustOLD  20117  metust  20118  metutopOLD  20132  psmetutop  20133  subgngp  20196  sranlm  20240  lssnlm  20256  icccmplem1  20374  icccmplem2  20375  icccmplem3  20376  reconnlem1  20378  reconnlem2  20379  reconn  20380  xrge0gsumle  20385  xrge0tsms  20386  metnrmlem1a  20409  metnrmlem1  20410  elcncf2  20441  cncfmet  20459  cncfmptid  20463  cnmpt2pc  20475  icccvx  20497  cnrehmeo  20500  cnheiborlem  20501  cnheibor  20502  cnllycmp  20503  bndth  20505  lebnumlem1  20508  lebnum  20511  htpycom  20523  htpyco1  20525  htpyco2  20526  htpycc  20527  phtpy01  20532  phtpycom  20535  phtpyco2  20537  phtpycc  20538  reparphti  20544  pcohtpylem  20566  clmvneg1  20638  clmmulg  20640  nmoleub3  20649  cvsmuleqdivd  20658  cvsdiveqd  20659  cphsubrglem  20671  cphreccllem  20672  cphdivcl  20676  cphsqrcl2  20680  cphsqrcl3  20681  cphipcl  20685  cphassr  20705  cph2ass  20706  tchcphlem3  20723  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  tchcph  20727  nmparlem  20729  iscfil3  20759  caublcls  20794  cmetss  20800  bcthlem3  20812  bcthlem4  20813  bcthlem5  20814  rrxdstprj1  20883  minveclem2  20888  minveclem3  20891  minveclem4a  20892  minveclem4b  20893  minveclem4  20894  minveclem7  20897  pjthlem1  20899  pjthlem2  20900  cldcss  20903  pmltpclem2  20908  ivthlem2  20911  ivthlem3  20912  ivth2  20914  ivthicc  20917  ovolctb  20948  ovolunlem1a  20954  ovolicc2lem4  20978  ovolicc2lem5  20979  ioombl1lem2  21015  ioombl1lem4  21017  dyadmaxlem  21052  dyadmbllem  21054  vitalilem2  21064  vitalilem3  21065  itg1val2  21137  itg1addlem1  21145  i1fmullem  21147  i1fadd  21148  limccl  21325  limcflflem  21330  limcflf  21331  limcmpt2  21334  cnplimc  21337  cnlimci  21339  limccnp2  21342  dvlem  21346  dvres2lem  21360  dvcnp2  21369  dvnadd  21378  cpncn  21385  dvaddbr  21387  dvmulbr  21388  dvcmul  21393  dvcobr  21395  dvcjbr  21398  dvcnvlem  21423  dvferm1lem  21431  dvferm1  21432  dvferm2lem  21433  dvferm2  21434  dvlip  21440  dvlipcn  21441  c1liplem1  21443  c1lip1  21444  dv11cn  21448  dvgt0lem1  21449  dvgt0  21451  dvlt0  21452  dvge0  21453  dvivthlem1  21455  dvivth  21457  dvne0  21458  lhop1lem  21460  lhop1  21461  lhop  21463  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcnvre  21466  dvcvx  21467  ftc1lem1  21482  ftc1a  21484  ftc1lem4  21486  ftc1lem5  21487  ftc1lem6  21488  ftc1  21489  ftc2ditglem  21492  ftc2ditg  21493  mdegcl  21515  deg1invg  21553  ply1divalg  21584  uc1pmon1p  21598  fta1glem1  21612  ig1peu  21618  ig1pdvds  21623  ig1prsp  21624  ply1lpir  21625  plyf  21641  plyeq0lem  21653  plypf1  21655  plyco  21684  dvply2g  21726  plydivlem4  21737  aannenlem2  21770  taylfvallem1  21797  tayl0  21802  taylplem1  21803  taylply2  21808  taylply  21809  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  ulmdvlem1  21840  ulmdvlem3  21842  pserulm  21862  pserdv  21869  abelthlem6  21876  abelthlem7  21878  efif1olem4  21976  eff1olem  21979  logccv  22083  xrlimcnp  22337  cvxcl  22353  scvxcvx  22354  jensenlem2  22356  jensen  22357  wilthlem2  22382  lgsquadlem3  22670  dchrisumlem2  22714  pntpbnd1  22810  pntibndlem2  22815  pntlem3  22833  tglineintmo  23016  f1otrg  23068  ttgbtwnid  23081  ttgcontlem1  23082  axlowdimlem17  23155  axcontlem4  23164  axcontlem9  23169  axcontlem10  23170  eengtrkg  23182  umgraex  23208  subgoid  23745  subgoinv  23746  sspz  24084  ubthlem2  24223  minvecolem2  24227  minvecolem3  24228  minvecolem4b  24230  minvecolem7  24235  occllem  24657  pjhcl  24755  pjpjpre  24773  chscllem2  24992  chscllem3  24993  chscllem4  24994  shatomistici  25716  sumdmdlem2  25774  elovimad  25907  opfv  25914  xrofsup  26006  ssnnssfz  26027  ressprs  26067  toslublem  26079  tosglblem  26081  submomnd  26124  gsumle  26197  gsummptf1o  26198  gsumvsca1  26202  gsumvsca2  26203  xrge0tsmsd  26204  suborng  26234  metideq  26272  xpinpreima2  26289  tpr2rico  26294  ordtconlem1  26306  lmxrge0  26334  lmdvg  26335  ind1  26427  esumcl  26438  gsumesum  26462  esumlub  26463  esumfsup  26471  esumpcvgval  26479  esumpmono  26480  esumcvg  26487  elsigagen2  26543  elsx  26560  measinb  26587  volmeas  26599  imambfm  26629  cnmbfm  26630  oms0  26662  omsmon  26663  sibfinima  26677  sibfof  26678  eulerpartlemgvv  26711  eulerpartlemgs2  26715  orvcoel  26796  orvccel  26797  ballotlemsdom  26846  ballotlemfrceq  26863  signstfvp  26924  signstfvc  26927  signsvfn  26935  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamucov  26976  erdsze2lem2  27044  conpcon  27076  txsconlem  27081  cvxpcon  27083  cvxscon  27084  cnllyscon  27086  rescon  27087  cvmsf1o  27113  cvmfolem  27120  cvmliftmolem1  27122  cvmliftmolem2  27123  cvmliftlem3  27128  cvmliftlem6  27131  cvmliftlem7  27132  cvmliftlem8  27133  cvmlift2lem9a  27144  cvmlift2lem9  27152  cvmlift2lem11  27154  cvmlift2lem12  27155  cvmliftphtlem  27158  cvmlift3lem6  27165  cvmlift3lem7  27166  prodmolem2a  27398  fprodcl2lem  27414  nodenselem3  27775  linethru  28135  heicant  28379  cnambfre  28393  ftc1cnnclem  28418  ftc1cnnc  28419  ivthALT  28483  comppfsc  28532  neibastop1  28533  neibastop2lem  28534  filnetlem3  28554  sdclem2  28591  caures  28609  sstotbnd2  28626  ssbnd  28640  totbndbnd  28641  prdsbnd  28645  prdstotbnd  28646  prdsbnd2  28647  heiborlem3  28665  heiborlem5  28667  heiborlem6  28668  heiborlem8  28670  reheibor  28691  istopclsd  28989  isnacs3  28999  diophrw  29050  rencldnfilem  29112  pellfundglb  29179  pellfundex  29180  pellfund14  29192  pellfund14b  29193  rmspecfund  29203  rmxyelqirr  29204  setindtr  29326  aomclem2  29361  kelac2  29371  isnumbasgrplem2  29413  hbtlem2  29433  hbtlem4  29435  hbtlem5  29437  cnsrexpcl  29475  cnsrplycl  29477  rngunsnply  29483  mon1psubm  29527  ubelsupr  29695  cncmpmax  29707  climinf  29732  climsuse  29734  stoweidlem7  29755  stoweidlem11  29759  stoweidlem26  29774  stoweidlem29  29777  stoweidlem31  29779  stoweidlem34  29782  stoweidlem36  29784  stoweidlem46  29794  stoweidlem52  29800  stoweidlem53  29801  stoweid  29811  extwwlkfablem2  30624  ssnn0ssfz  30693  supgtoreq  30694  supfirege  30695  fsuppmapnn0fiublem  30747  scmatdmat  30806  iunconlem2  31558  bnj907  31845  bnj1121  31863  bnj1128  31868  bnj1175  31882  bnj1177  31884  bnj1417  31919  lshpnel  32468  lshpnelb  32469  lsatlssel  32482  lsmsat  32493  lssats  32497  lrelat  32499  lsmcv2  32514  lcvexchlem1  32519  lcvexchlem2  32520  lcvexchlem3  32521  lcvexchlem4  32522  lcvexchlem5  32523  lcv1  32526  lcv2  32527  lsatexch  32528  lsatcv0eq  32532  lsatcvatlem  32534  lsatcvat  32535  lsatcvat3  32537  l1cvat  32540  lkrlsp  32587  lshpsmreu  32594  lshpkrlem5  32599  paddcom  33297  paddasslem11  33314  paddasslem12  33315  paddasslem13  33316  pmodlem1  33330  pclfinN  33384  osumcllem6N  33445  osumcllem9N  33448  osumcllem11N  33450  pexmidlem3N  33456  dia2dimlem5  34553  dia2dimlem9  34557  dvhopellsm  34602  diblss  34655  diblsmopel  34656  dicvaddcl  34675  dicvscacl  34676  cdlemn5pre  34685  cdlemn11b  34693  cdlemn11c  34694  dihjustlem  34701  dihord1  34703  dihord2a  34704  dihord2b  34705  dihord11b  34707  dihord11c  34709  dihopcl  34738  dihord6apre  34741  dihord5b  34744  dihord5apre  34747  dihglblem2aN  34778  dihglblem2N  34779  dihglblem3N  34780  dihglblem4  34782  dihglblem5  34783  dihglbcpreN  34785  dihjatc3  34798  dihmeetlem9N  34800  dihjatcclem1  34903  dihjatcclem2  34904  dihjat  34908  dvh3dim3N  34934  dochexmidlem2  34946  dochexmidlem6  34950  dochexmidlem7  34951  dochsnkr  34957  dochfln0  34962  lcfl6lem  34983  lcfl6  34985  lclkrlem2b  34993  lclkrlem2f  34997  lclkrlem2v  35013  lclkrslem2  35023  lcfrlem4  35030  lcfrlem16  35043  lcfrlem23  35050  lcfrlem25  35052  lcfrlem31  35058  lcfrlem33  35060  lcfrlem35  35062  lcdvbaselfl  35080  mapdrvallem2  35130  mapdlsm  35149  mapdpglem3  35160  mapdpglem9  35165  mapdpglem14  35170  mapdpglem17N  35173  mapdpglem18  35174  mapdpglem21  35177  mapdindp0  35204  lspindp5  35255  hdmaprnlem4tN  35340  hdmaprnlem4N  35341  hdmaprnlem3eN  35346  hdmapinvlem1  35406  hdmapinvlem2  35407  hdmapinvlem3  35408  hdmapinvlem4  35409  hdmapglem5  35410  hdmapglem7a  35415  hdmapglem7b  35416  hdmapglem7  35417
  Copyright terms: Public domain W3C validator