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

Theorem sseldd 3181
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 3179 . 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 1684    C_ wss 3152
This theorem is referenced by:  ordunel  4618  sofld  5121  soisores  5824  riotass  6333  tfrlem13  6406  omordi  6564  oeeulem  6599  oeeui  6600  eroveu  6753  eroprf  6756  ixpssmapg  6846  omxpenlem  6963  nnunifi  7108  unifpw  7158  dffi3  7184  ordtypelem6  7238  oismo  7255  unxpwdom2  7302  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cantnflem4  7394  cnfcomlem  7402  cnfcom  7403  cnfcom3lem  7406  cnfcom3  7407  cnfcom3clem  7408  r1sscl  7457  tz9.12lem3  7461  pwwf  7479  rankonidlem  7500  r1pw  7517  r0weon  7640  dfac8clem  7659  iunfictbso  7741  dfac12lem2  7770  infpssrlem3  7931  ssfin4  7936  fin23lem11  7943  fin23lem24  7948  fin23lem26  7951  fin23lem23  7952  fin23lem22  7953  fin23lem27  7954  fin1a2lem9  8034  fin1a2lem11  8036  hsmexlem3  8054  ttukeylem6  8141  ttukeylem7  8142  iunfo  8161  fpwwe2lem6  8257  fpwwe2lem9  8260  fpwwe2lem12  8263  pwfseqlem5  8285  gch2  8301  wunss  8334  wunf  8349  r1limwun  8358  wunex2  8360  inttsk  8396  tskuni  8405  wloglei  9305  suprzcl  10091  suprzub  10309  uzwo3  10311  rpnnen1lem5  10346  fzssp1  10834  elfzoelz  10875  fzofzp1  10916  fzostep1  10922  fseqsupcl  11039  sermono  11078  seqf1olem2a  11084  seqf1olem2  11086  bcm1k  11327  seqcoll  11401  seqcoll2  11402  swrdcl  11452  splfv1  11470  splfv2a  11471  rlimclim1  12019  rlimresb  12039  rlimcld2  12052  o1rlimmul  12092  lo1le  12125  isercolllem2  12139  caucvgrlem  12145  summolem2a  12188  fsumcvg3  12202  fsumcl2lem  12204  fsum0diaglem  12239  mertenslem2  12341  bitsfzolem  12625  bitsfzo  12626  vdwlem1  13028  vdwlem2  13029  vdwlem5  13032  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwlem11  13038  0ram  13067  0ramcl  13070  ramub1lem1  13073  strssd  13182  imasvscafn  13439  mrieqvlemd  13531  mrieqv2d  13541  mreexexlem2d  13547  isacs2  13555  ssctr  13702  ssceq  13703  subcss2  13717  subccatid  13720  fullresc  13725  funcres  13770  ffthiso  13803  rescfth  13811  ressffth  13812  resssetc  13924  funcsetcres2  13925  resscatc  13937  catcisolem  13938  catciso  13939  yonedalem1  14046  yonffthlem  14056  yoniso  14059  lubun  14227  ipodrsima  14268  isacs3lem  14269  acsmapd  14281  resmhm  14436  mhmima  14440  gsumress  14454  gsumval2  14460  gsumwspan  14468  frmdss2  14485  mulgnnsubcl  14579  mulgnn0subcl  14580  mulgsubcl  14581  mulgpropd  14600  submmulg  14602  subg0  14627  subgsubcl  14632  subgsub  14633  subgmulg  14635  issubg4  14638  nsgconj  14650  ssnmz  14659  ghmnsgima  14706  subgga  14754  gasubg  14756  cntzrcl  14803  cntrsubgnsg  14816  odf1o1  14883  odcau  14915  sylow2blem1  14931  sylow2blem2  14932  sylow2blem3  14933  sylow3lem2  14939  lsmub1x  14957  lsmsubm  14964  lsmsubg  14965  lsmass  14979  lsmmod  14984  lsmpropd  14986  lsmdisj2  14991  subgdisj1  15000  subgdisj2  15001  pj1id  15008  pj1ghm  15012  efgsp1  15046  efgsres  15047  efgsfo  15048  efgredlemf  15050  efgredlemd  15053  subgabl  15132  lsmcomx  15148  gsumzadd  15204  gsumzsplit  15206  dprdfcntz  15250  dprdfadd  15255  dprdfeq0  15257  dprdlub  15261  dprdres  15263  dprd2dlem2  15275  dprd2da  15277  dmdprdsplit2lem  15280  dpjrid  15297  ablfac1b  15305  ablfac1eulem  15307  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem4  15313  pgpfac1lem5  15314  isdrng2  15522  subrguss  15560  subrginv  15561  subrgdv  15562  issubdrg  15570  abvres  15604  islss3  15716  lspsnel3  15748  lsspropd  15774  reslmhm  15809  lbspss  15835  lsmsp  15839  lspprabs  15848  pj1lmhm  15853  pj1lmhm2  15854  lspindpi  15885  lvecindp  15891  lsmcv  15894  lspsolvlem  15895  lspsolv  15896  lspsnat  15898  lsppratlem1  15900  lsppratlem3  15902  lsppratlem4  15903  islbs2  15907  lbsextlem2  15912  lbsextlem3  15913  domnrrg  16041  issubassa  16064  sraassa  16065  issubassa2  16084  resspsradd  16160  resspsrmul  16161  resspsrvsca  16162  mplbas2  16212  mplind  16243  qsssubdrg  16431  cnsubrg  16432  zlpirlem3  16443  lsmcss  16592  cssmre  16593  pjdm2  16611  pjf2  16614  pjfo  16615  ocvpj  16617  obselocv  16628  toponmre  16830  topssnei  16861  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  cnss1  17005  cnprest  17017  lmres  17028  iuncon  17154  concompcld  17160  concompclo  17161  2ndcctbss  17181  2ndcdisj  17182  dis2ndc  17186  llycmpkgen2  17245  1stckgenlem  17248  kgen2cn  17254  ptbasfi  17276  ptopn  17278  txopn  17297  ptpjcn  17305  ptpjopn  17306  txcnp  17314  ptrescn  17333  txtube  17334  xkopjcn  17350  kqreglem2  17433  reghmph  17484  isufil2  17603  ssufl  17613  ufileu  17614  filufint  17615  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  flimfil  17664  flimcf  17677  flimclslem  17679  hauspwpwf1  17682  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  cnpfcfi  17735  cnpfcf  17736  alexsublem  17738  alexsubALTlem3  17743  alexsubALTlem4  17744  subgntr  17789  tsmsmhm  17828  tsmsadd  17829  tsmssub  17831  tgptsmscls  17832  tsmsxp  17837  invrcn  17863  xmetres2  17925  prdsmet  17934  ressprdsds  17935  blin2  17975  blopn  18046  lpbl  18049  met2ndci  18068  prdsxmslem2  18075  subgngp  18151  sranlm  18195  lssnlm  18211  icccmplem1  18327  icccmplem2  18328  icccmplem3  18329  reconnlem1  18331  reconnlem2  18332  reconn  18333  xrge0gsumle  18338  xrge0tsms  18339  metnrmlem1a  18362  metnrmlem1  18363  elcncf2  18394  cncfmet  18412  cncfmptid  18416  cnmpt2pc  18426  icccvx  18448  cnrehmeo  18451  cnheiborlem  18452  cnheibor  18453  cnllycmp  18454  bndth  18456  lebnumlem1  18459  lebnum  18462  htpycom  18474  htpyco1  18476  htpyco2  18477  htpycc  18478  phtpy01  18483  phtpycom  18486  phtpyco2  18488  phtpycc  18489  reparphti  18495  pcohtpylem  18517  clmvneg1  18589  clmmulg  18591  nmoleub3  18600  cphsubrglem  18613  cphreccllem  18614  cphdivcl  18618  cphsqrcl2  18622  cphsqrcl3  18623  cphipcl  18627  cphassr  18647  cph2ass  18648  tchcphlem3  18663  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  tchcph  18667  nmparlem  18669  iscfil3  18699  caublcls  18734  cmetss  18740  bcthlem3  18748  bcthlem4  18749  bcthlem5  18750  minveclem2  18790  minveclem3  18793  minveclem4a  18794  minveclem4b  18795  minveclem4  18796  minveclem7  18799  pjthlem1  18801  pjthlem2  18802  cldcss  18805  pmltpclem2  18809  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ivthicc  18818  ovolctb  18849  ovolunlem1a  18855  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1lem2  18916  ioombl1lem4  18918  dyadmaxlem  18952  dyadmbllem  18954  vitalilem2  18964  vitalilem3  18965  itg1val2  19039  itg1addlem1  19047  i1fmullem  19049  i1fadd  19050  limccl  19225  limcflflem  19230  limcflf  19231  limcmpt2  19234  cnplimc  19237  cnlimci  19239  limccnp2  19242  dvlem  19246  dvres2lem  19260  dvcnp2  19269  dvnadd  19278  cpncn  19285  dvaddbr  19287  dvmulbr  19288  dvcmul  19293  dvcobr  19295  dvcjbr  19298  dvcnvlem  19323  dvferm1lem  19331  dvferm1  19332  dvferm2lem  19333  dvferm2  19334  dvlip  19340  dvlipcn  19341  c1liplem1  19343  c1lip1  19344  dv11cn  19348  dvgt0lem1  19349  dvgt0  19351  dvlt0  19352  dvge0  19353  dvivthlem1  19355  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  dvcvx  19367  ftc1lem1  19382  ftc1a  19384  ftc1lem4  19386  ftc1lem5  19387  ftc1lem6  19388  ftc1  19389  ftc2ditglem  19392  ftc2ditg  19393  mpff  19425  mpfaddcl  19426  mpfmulcl  19427  pf1f  19433  mdegcl  19455  deg1invg  19492  ply1divalg  19523  uc1pmon1p  19537  fta1glem1  19551  ig1peu  19557  ig1pdvds  19562  ig1prsp  19563  ply1lpir  19564  plyf  19580  plyeq0lem  19592  plypf1  19594  plyco  19623  dvply2g  19665  plydivlem4  19676  aannenlem2  19709  taylfvallem1  19736  tayl0  19741  taylplem1  19742  taylply2  19747  taylply  19748  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  ulmdvlem1  19777  ulmdvlem3  19779  pserulm  19798  pserdv  19805  abelthlem6  19812  abelthlem7  19814  efif1olem4  19907  eff1olem  19910  logccv  20010  rlimcnp  20260  xrlimcnp  20263  cvxcl  20279  scvxcvx  20280  jensenlem2  20282  jensen  20283  wilthlem2  20307  lgsquadlem3  20595  dchrisumlem2  20639  pntpbnd1  20735  pntibndlem2  20740  pntlem3  20758  subgoid  20974  subgoinv  20975  sspz  21311  ubthlem2  21450  minvecolem2  21454  minvecolem3  21455  minvecolem4b  21457  minvecolem7  21462  occllem  21882  pjhcl  21980  pjpjpre  21998  chscllem2  22217  chscllem3  22218  chscllem4  22219  shatomistici  22941  sumdmdlem2  22999  ballotlemsdom  23070  ballotlemfrceq  23087  elovimad  23205  xrofsup  23255  ssnnssfz  23277  xpinpreima2  23291  tpr2rico  23296  lmxrge0  23375  lmdvg  23376  gsumpropd2lem  23379  xrge0tsmsd  23382  esumcl  23413  esumpcvgval  23446  esumpmono  23447  esumcvg  23454  elsigagen2  23509  elsx  23525  measinb  23548  imambfm  23567  cnmbfm  23568  ind1  23602  orvcoel  23662  orvccel  23663  erdsze2lem2  23735  conpcon  23766  txsconlem  23771  cvxpcon  23773  cvxscon  23774  cnllyscon  23776  rescon  23777  cvmsf1o  23803  cvmfolem  23810  cvmliftmolem1  23812  cvmliftmolem2  23813  cvmliftlem3  23818  cvmliftlem6  23821  cvmliftlem7  23822  cvmliftlem8  23823  cvmlift2lem9a  23834  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmliftphtlem  23848  cvmlift3lem6  23855  cvmlift3lem7  23856  umgraex  23875  nodenselem3  24337  axlowdimlem17  24586  axcontlem4  24595  axcontlem9  24600  axcontlem10  24601  linethru  24776  uninqs  25039  cnrsfin  25525  cnrscoa  25526  intopcoaconlem3b  25538  exopcopn  25572  islimrs3  25581  cardtar  25904  lineval5a  26088  lineval6a  26089  ivthALT  26258  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  filnetlem3  26329  sdclem2  26452  caures  26476  sstotbnd2  26498  ssbnd  26512  totbndbnd  26513  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  heiborlem3  26537  heiborlem5  26539  heiborlem6  26540  heiborlem8  26542  reheibor  26563  istopclsd  26775  isnacs3  26785  diophrw  26838  rencldnfilem  26903  pellfundglb  26970  pellfundex  26971  pellfund14  26983  pellfund14b  26984  rmspecfund  26994  rmxyelqirr  26995  setindtr  27117  aomclem2  27152  kelac2  27163  frlmplusgval  27229  frlmvscafval  27230  frlmssuvc1  27246  frlmsslsp  27248  isnumbasgrplem2  27269  lindff1  27290  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  cnsrexpcl  27370  cnsrplycl  27372  rngunsnply  27378  pmtrf  27397  pmtrfinv  27402  symggen  27411  psgnunilem1  27416  psgnunilem5  27417  mon1psubm  27525  cncmpmax  27703  climinf  27732  climsuse  27734  stoweidlem11  27760  stoweidlem29  27778  stoweidlem34  27783  stoweidlem46  27795  bnj907  28997  bnj1121  29015  bnj1128  29020  bnj1175  29034  bnj1177  29036  bnj1417  29071  lubunNEW  29163  lshpnel  29173  lshpnelb  29174  lsatlssel  29187  lsmsat  29198  lssats  29202  lrelat  29204  lsmcv2  29219  lcvexchlem1  29224  lcvexchlem2  29225  lcvexchlem3  29226  lcvexchlem4  29227  lcvexchlem5  29228  lcv1  29231  lcv2  29232  lsatexch  29233  lsatcv0eq  29237  lsatcvatlem  29239  lsatcvat  29240  lsatcvat3  29242  l1cvat  29245  lkrlsp  29292  lshpsmreu  29299  lshpkrlem5  29304  paddcom  30002  paddasslem11  30019  paddasslem12  30020  paddasslem13  30021  pmodlem1  30035  pclfinN  30089  osumcllem6N  30150  osumcllem9N  30153  osumcllem11N  30155  pexmidlem3N  30161  dia2dimlem5  31258  dia2dimlem9  31262  dvhopellsm  31307  diblss  31360  diblsmopel  31361  dicvaddcl  31380  dicvscacl  31381  cdlemn5pre  31390  cdlemn11b  31398  cdlemn11c  31399  dihjustlem  31406  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord11b  31412  dihord11c  31414  dihopcl  31443  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dihglblem2aN  31483  dihglblem2N  31484  dihglblem3N  31485  dihglblem4  31487  dihglblem5  31488  dihglbcpreN  31490  dihjatc3  31503  dihmeetlem9N  31505  dihjatcclem1  31608  dihjatcclem2  31609  dihjat  31613  dvh3dim3N  31639  dochexmidlem2  31651  dochexmidlem6  31655  dochexmidlem7  31656  dochsnkr  31662  dochfln0  31667  lcfl6lem  31688  lcfl6  31690  lclkrlem2b  31698  lclkrlem2f  31702  lclkrlem2v  31718  lclkrslem2  31728  lcfrlem4  31735  lcfrlem16  31748  lcfrlem23  31755  lcfrlem25  31757  lcfrlem31  31763  lcfrlem33  31765  lcfrlem35  31767  lcdvbaselfl  31785  mapdrvallem2  31835  mapdlsm  31854  mapdpglem3  31865  mapdpglem9  31870  mapdpglem14  31875  mapdpglem17N  31878  mapdpglem18  31879  mapdpglem21  31882  mapdindp0  31909  lspindp5  31960  hdmaprnlem4tN  32045  hdmaprnlem4N  32046  hdmaprnlem3eN  32051  hdmapinvlem1  32111  hdmapinvlem2  32112  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem5  32115  hdmapglem7a  32120  hdmapglem7b  32121  hdmapglem7  32122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator