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

Theorem sseldd 3194
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 3192 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
41, 3mpd 14 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  ordunel  4634  sofld  5137  soisores  5840  riotass  6349  tfrlem13  6422  omordi  6580  oeeulem  6615  oeeui  6616  eroveu  6769  eroprf  6772  ixpssmapg  6862  omxpenlem  6979  nnunifi  7124  unifpw  7174  dffi3  7200  ordtypelem6  7254  oismo  7271  unxpwdom2  7318  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cantnflem4  7410  cnfcomlem  7418  cnfcom  7419  cnfcom3lem  7422  cnfcom3  7423  cnfcom3clem  7424  r1sscl  7473  tz9.12lem3  7477  pwwf  7495  rankonidlem  7516  r1pw  7533  r0weon  7656  dfac8clem  7675  iunfictbso  7757  dfac12lem2  7786  infpssrlem3  7947  ssfin4  7952  fin23lem11  7959  fin23lem24  7964  fin23lem26  7967  fin23lem23  7968  fin23lem22  7969  fin23lem27  7970  fin1a2lem9  8050  fin1a2lem11  8052  hsmexlem3  8070  ttukeylem6  8157  ttukeylem7  8158  iunfo  8177  fpwwe2lem6  8273  fpwwe2lem9  8276  fpwwe2lem12  8279  pwfseqlem5  8301  gch2  8317  wunss  8350  wunf  8365  r1limwun  8374  wunex2  8376  inttsk  8412  tskuni  8421  wloglei  9321  suprzcl  10107  suprzub  10325  uzwo3  10327  rpnnen1lem5  10362  fzssp1  10850  elfzoelz  10891  fzofzp1  10932  fzostep1  10938  fseqsupcl  11055  sermono  11094  seqf1olem2a  11100  seqf1olem2  11102  bcm1k  11343  seqcoll  11417  seqcoll2  11418  swrdcl  11468  splfv1  11486  splfv2a  11487  rlimclim1  12035  rlimresb  12055  rlimcld2  12068  o1rlimmul  12108  lo1le  12141  isercolllem2  12155  caucvgrlem  12161  summolem2a  12204  fsumcvg3  12218  fsumcl2lem  12220  fsum0diaglem  12255  mertenslem2  12357  bitsfzolem  12641  bitsfzo  12642  vdwlem1  13044  vdwlem2  13045  vdwlem5  13048  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  vdwlem11  13054  0ram  13083  0ramcl  13086  ramub1lem1  13089  strssd  13198  imasvscafn  13455  mrieqvlemd  13547  mrieqv2d  13557  mreexexlem2d  13563  isacs2  13571  ssctr  13718  ssceq  13719  subcss2  13733  subccatid  13736  fullresc  13741  funcres  13786  ffthiso  13819  rescfth  13827  ressffth  13828  resssetc  13940  funcsetcres2  13941  resscatc  13953  catcisolem  13954  catciso  13955  yonedalem1  14062  yonffthlem  14072  yoniso  14075  lubun  14243  ipodrsima  14284  isacs3lem  14285  acsmapd  14297  resmhm  14452  mhmima  14456  gsumress  14470  gsumval2  14476  gsumwspan  14484  frmdss2  14501  mulgnnsubcl  14595  mulgnn0subcl  14596  mulgsubcl  14597  mulgpropd  14616  submmulg  14618  subg0  14643  subgsubcl  14648  subgsub  14649  subgmulg  14651  issubg4  14654  nsgconj  14666  ssnmz  14675  ghmnsgima  14722  subgga  14770  gasubg  14772  cntzrcl  14819  cntrsubgnsg  14832  odf1o1  14899  odcau  14931  sylow2blem1  14947  sylow2blem2  14948  sylow2blem3  14949  sylow3lem2  14955  lsmub1x  14973  lsmsubm  14980  lsmsubg  14981  lsmass  14995  lsmmod  15000  lsmpropd  15002  lsmdisj2  15007  subgdisj1  15016  subgdisj2  15017  pj1id  15024  pj1ghm  15028  efgsp1  15062  efgsres  15063  efgsfo  15064  efgredlemf  15066  efgredlemd  15069  subgabl  15148  lsmcomx  15164  gsumzadd  15220  gsumzsplit  15222  dprdfcntz  15266  dprdfadd  15271  dprdfeq0  15273  dprdlub  15277  dprdres  15279  dprd2dlem2  15291  dprd2da  15293  dmdprdsplit2lem  15296  dpjrid  15313  ablfac1b  15321  ablfac1eulem  15323  pgpfac1lem1  15325  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem4  15329  pgpfac1lem5  15330  isdrng2  15538  subrguss  15576  subrginv  15577  subrgdv  15578  issubdrg  15586  abvres  15620  islss3  15732  lspsnel3  15764  lsspropd  15790  reslmhm  15825  lbspss  15851  lsmsp  15855  lspprabs  15864  pj1lmhm  15869  pj1lmhm2  15870  lspindpi  15901  lvecindp  15907  lsmcv  15910  lspsolvlem  15911  lspsolv  15912  lspsnat  15914  lsppratlem1  15916  lsppratlem3  15918  lsppratlem4  15919  islbs2  15923  lbsextlem2  15928  lbsextlem3  15929  domnrrg  16057  issubassa  16080  sraassa  16081  issubassa2  16100  resspsradd  16176  resspsrmul  16177  resspsrvsca  16178  mplbas2  16228  mplind  16259  qsssubdrg  16447  cnsubrg  16448  zlpirlem3  16459  lsmcss  16608  cssmre  16609  pjdm2  16627  pjf2  16630  pjfo  16631  ocvpj  16633  obselocv  16644  toponmre  16846  topssnei  16877  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  cnss1  17021  cnprest  17033  lmres  17044  iuncon  17170  concompcld  17176  concompclo  17177  2ndcctbss  17197  2ndcdisj  17198  dis2ndc  17202  llycmpkgen2  17261  1stckgenlem  17264  kgen2cn  17270  ptbasfi  17292  ptopn  17294  txopn  17313  ptpjcn  17321  ptpjopn  17322  txcnp  17330  ptrescn  17349  txtube  17350  xkopjcn  17366  kqreglem2  17449  reghmph  17500  isufil2  17619  ssufl  17629  ufileu  17630  filufint  17631  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  flimfil  17680  flimcf  17693  flimclslem  17695  hauspwpwf1  17698  fclscf  17736  fclsfnflim  17738  flimfnfcls  17739  cnpfcfi  17751  cnpfcf  17752  alexsublem  17754  alexsubALTlem3  17759  alexsubALTlem4  17760  subgntr  17805  tsmsmhm  17844  tsmsadd  17845  tsmssub  17847  tgptsmscls  17848  tsmsxp  17853  invrcn  17879  xmetres2  17941  prdsmet  17950  ressprdsds  17951  blin2  17991  blopn  18062  lpbl  18065  met2ndci  18084  prdsxmslem2  18091  subgngp  18167  sranlm  18211  lssnlm  18227  icccmplem1  18343  icccmplem2  18344  icccmplem3  18345  reconnlem1  18347  reconnlem2  18348  reconn  18349  xrge0gsumle  18354  xrge0tsms  18355  metnrmlem1a  18378  metnrmlem1  18379  elcncf2  18410  cncfmet  18428  cncfmptid  18432  cnmpt2pc  18442  icccvx  18464  cnrehmeo  18467  cnheiborlem  18468  cnheibor  18469  cnllycmp  18470  bndth  18472  lebnumlem1  18475  lebnum  18478  htpycom  18490  htpyco1  18492  htpyco2  18493  htpycc  18494  phtpy01  18499  phtpycom  18502  phtpyco2  18504  phtpycc  18505  reparphti  18511  pcohtpylem  18533  clmvneg1  18605  clmmulg  18607  nmoleub3  18616  cphsubrglem  18629  cphreccllem  18630  cphdivcl  18634  cphsqrcl2  18638  cphsqrcl3  18639  cphipcl  18643  cphassr  18663  cph2ass  18664  tchcphlem3  18679  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  tchcph  18683  nmparlem  18685  iscfil3  18715  caublcls  18750  cmetss  18756  bcthlem3  18764  bcthlem4  18765  bcthlem5  18766  minveclem2  18806  minveclem3  18809  minveclem4a  18810  minveclem4b  18811  minveclem4  18812  minveclem7  18815  pjthlem1  18817  pjthlem2  18818  cldcss  18821  pmltpclem2  18825  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ivthicc  18834  ovolctb  18865  ovolunlem1a  18871  ovolicc2lem4  18895  ovolicc2lem5  18896  ioombl1lem2  18932  ioombl1lem4  18934  dyadmaxlem  18968  dyadmbllem  18970  vitalilem2  18980  vitalilem3  18981  itg1val2  19055  itg1addlem1  19063  i1fmullem  19065  i1fadd  19066  limccl  19241  limcflflem  19246  limcflf  19247  limcmpt2  19250  cnplimc  19253  cnlimci  19255  limccnp2  19258  dvlem  19262  dvres2lem  19276  dvcnp2  19285  dvnadd  19294  cpncn  19301  dvaddbr  19303  dvmulbr  19304  dvcmul  19309  dvcobr  19311  dvcjbr  19314  dvcnvlem  19339  dvferm1lem  19347  dvferm1  19348  dvferm2lem  19349  dvferm2  19350  dvlip  19356  dvlipcn  19357  c1liplem1  19359  c1lip1  19360  dv11cn  19364  dvgt0lem1  19365  dvgt0  19367  dvlt0  19368  dvge0  19369  dvivthlem1  19371  dvivth  19373  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  dvcvx  19383  ftc1lem1  19398  ftc1a  19400  ftc1lem4  19402  ftc1lem5  19403  ftc1lem6  19404  ftc1  19405  ftc2ditglem  19408  ftc2ditg  19409  mpff  19441  mpfaddcl  19442  mpfmulcl  19443  pf1f  19449  mdegcl  19471  deg1invg  19508  ply1divalg  19539  uc1pmon1p  19553  fta1glem1  19567  ig1peu  19573  ig1pdvds  19578  ig1prsp  19579  ply1lpir  19580  plyf  19596  plyeq0lem  19608  plypf1  19610  plyco  19639  dvply2g  19681  plydivlem4  19692  aannenlem2  19725  taylfvallem1  19752  tayl0  19757  taylplem1  19758  taylply2  19763  taylply  19764  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  ulmdvlem1  19793  ulmdvlem3  19795  pserulm  19814  pserdv  19821  abelthlem6  19828  abelthlem7  19830  efif1olem4  19923  eff1olem  19926  logccv  20026  rlimcnp  20276  xrlimcnp  20279  cvxcl  20295  scvxcvx  20296  jensenlem2  20298  jensen  20299  wilthlem2  20323  lgsquadlem3  20611  dchrisumlem2  20655  pntpbnd1  20751  pntibndlem2  20756  pntlem3  20774  subgoid  20990  subgoinv  20991  sspz  21327  ubthlem2  21466  minvecolem2  21470  minvecolem3  21471  minvecolem4b  21473  minvecolem7  21478  occllem  21898  pjhcl  21996  pjpjpre  22014  chscllem2  22233  chscllem3  22234  chscllem4  22235  shatomistici  22957  sumdmdlem2  23015  ballotlemsdom  23086  ballotlemfrceq  23103  elovimad  23220  xrofsup  23270  ssnnssfz  23292  xpinpreima2  23306  tpr2rico  23311  lmxrge0  23390  lmdvg  23391  gsumpropd2lem  23394  xrge0tsmsd  23397  esumcl  23428  esumpcvgval  23461  esumpmono  23462  esumcvg  23469  elsigagen2  23524  elsx  23540  measinb  23563  imambfm  23582  cnmbfm  23583  ind1  23617  orvcoel  23677  orvccel  23678  erdsze2lem2  23750  conpcon  23781  txsconlem  23786  cvxpcon  23788  cvxscon  23789  cnllyscon  23791  rescon  23792  cvmsf1o  23818  cvmfolem  23825  cvmliftmolem1  23827  cvmliftmolem2  23828  cvmliftlem3  23833  cvmliftlem6  23836  cvmliftlem7  23837  cvmliftlem8  23838  cvmlift2lem9a  23849  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmliftphtlem  23863  cvmlift3lem6  23870  cvmlift3lem7  23871  umgraex  23890  prodmolem2a  24157  nodenselem3  24408  axlowdimlem17  24658  axcontlem4  24667  axcontlem9  24672  axcontlem10  24673  linethru  24848  ftc1cnnclem  25024  ftc1cnnc  25025  uninqs  25142  cnrsfin  25628  cnrscoa  25629  intopcoaconlem3b  25641  exopcopn  25675  islimrs3  25684  cardtar  26007  lineval5a  26191  lineval6a  26192  ivthALT  26361  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  filnetlem3  26432  sdclem2  26555  caures  26579  sstotbnd2  26601  ssbnd  26615  totbndbnd  26616  prdsbnd  26620  prdstotbnd  26621  prdsbnd2  26622  heiborlem3  26640  heiborlem5  26642  heiborlem6  26643  heiborlem8  26645  reheibor  26666  istopclsd  26878  isnacs3  26888  diophrw  26941  rencldnfilem  27006  pellfundglb  27073  pellfundex  27074  pellfund14  27086  pellfund14b  27087  rmspecfund  27097  rmxyelqirr  27098  setindtr  27220  aomclem2  27255  kelac2  27266  frlmplusgval  27332  frlmvscafval  27333  frlmssuvc1  27349  frlmsslsp  27351  isnumbasgrplem2  27372  lindff1  27393  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  cnsrexpcl  27473  cnsrplycl  27475  rngunsnply  27481  pmtrf  27500  pmtrfinv  27505  symggen  27514  psgnunilem1  27519  psgnunilem5  27520  mon1psubm  27628  cncmpmax  27806  climinf  27835  climsuse  27837  stoweidlem11  27863  stoweidlem29  27881  stoweidlem34  27886  stoweidlem46  27898  bnj907  29313  bnj1121  29331  bnj1128  29336  bnj1175  29350  bnj1177  29352  bnj1417  29387  lubunNEW  29785  lshpnel  29795  lshpnelb  29796  lsatlssel  29809  lsmsat  29820  lssats  29824  lrelat  29826  lsmcv2  29841  lcvexchlem1  29846  lcvexchlem2  29847  lcvexchlem3  29848  lcvexchlem4  29849  lcvexchlem5  29850  lcv1  29853  lcv2  29854  lsatexch  29855  lsatcv0eq  29859  lsatcvatlem  29861  lsatcvat  29862  lsatcvat3  29864  l1cvat  29867  lkrlsp  29914  lshpsmreu  29921  lshpkrlem5  29926  paddcom  30624  paddasslem11  30641  paddasslem12  30642  paddasslem13  30643  pmodlem1  30657  pclfinN  30711  osumcllem6N  30772  osumcllem9N  30775  osumcllem11N  30777  pexmidlem3N  30783  dia2dimlem5  31880  dia2dimlem9  31884  dvhopellsm  31929  diblss  31982  diblsmopel  31983  dicvaddcl  32002  dicvscacl  32003  cdlemn5pre  32012  cdlemn11b  32020  cdlemn11c  32021  dihjustlem  32028  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord11b  32034  dihord11c  32036  dihopcl  32065  dihord6apre  32068  dihord5b  32071  dihord5apre  32074  dihglblem2aN  32105  dihglblem2N  32106  dihglblem3N  32107  dihglblem4  32109  dihglblem5  32110  dihglbcpreN  32112  dihjatc3  32125  dihmeetlem9N  32127  dihjatcclem1  32230  dihjatcclem2  32231  dihjat  32235  dvh3dim3N  32261  dochexmidlem2  32273  dochexmidlem6  32277  dochexmidlem7  32278  dochsnkr  32284  dochfln0  32289  lcfl6lem  32310  lcfl6  32312  lclkrlem2b  32320  lclkrlem2f  32324  lclkrlem2v  32340  lclkrslem2  32350  lcfrlem4  32357  lcfrlem16  32370  lcfrlem23  32377  lcfrlem25  32379  lcfrlem31  32385  lcfrlem33  32387  lcfrlem35  32389  lcdvbaselfl  32407  mapdrvallem2  32457  mapdlsm  32476  mapdpglem3  32487  mapdpglem9  32492  mapdpglem14  32497  mapdpglem17N  32500  mapdpglem18  32501  mapdpglem21  32504  mapdindp0  32531  lspindp5  32582  hdmaprnlem4tN  32667  hdmaprnlem4N  32668  hdmaprnlem3eN  32673  hdmapinvlem1  32733  hdmapinvlem2  32734  hdmapinvlem3  32735  hdmapinvlem4  32736  hdmapglem5  32737  hdmapglem7a  32742  hdmapglem7b  32743  hdmapglem7  32744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator