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

Theorem sseldi 3348
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
Hypotheses
Ref Expression
sseli.1  |-  A  C_  B
sseldi.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
sseldi  |-  ( ph  ->  C  e.  B )

Proof of Theorem sseldi
StepHypRef Expression
1 sseldi.2 . 2  |-  ( ph  ->  C  e.  A )
2 sseli.1 . . 3  |-  A  C_  B
32sseli 3346 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3syl 16 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  onfr  4622  suctr  4667  sofld  5320  fvrn0  5755  elmpt2cl  6290  ofrval  6317  mpt2xopn0yelv  6466  mpt2xopxnop0  6468  tpostpos  6501  opiota  6537  riotacl  6566  riotasbc  6567  smores  6616  tz7.44-2  6667  omopthlem2  6901  f1opwfi  7412  supub  7466  suplub  7467  ordtypelem3  7491  ordtypelem4  7492  ordtypelem6  7494  ordtypelem7  7495  wemapso2lem  7521  wemapso2  7523  unxpwdom2  7558  cantnfres  7635  wemapwe  7656  oef1o  7657  cnfcomlem  7658  r1pwss  7712  r1elwf  7724  rankr1ai  7726  r0weon  7896  infxpenlem  7897  acnlem  7931  acndom2  7937  infpwfien  7945  alephfp  7991  ackbij1b  8121  cflim2  8145  fin23lem26  8207  isf32lem5  8239  isf32lem7  8241  isf32lem8  8242  isf32lem9  8243  isfin1-3  8268  fin1a2lem9  8290  fin1a2lem11  8292  hsmexlem5  8312  zorn2lem3  8380  zorn2lem4  8381  zorn2lem5  8382  ttukeylem6  8396  ttukeylem7  8397  iundom2g  8417  fpwwe2lem12  8518  pwfseqlem3  8537  gch2  8556  wunom  8597  rexrd  9136  nnred  10017  nncnd  10018  un0addcl  10255  un0mulcl  10256  nnnn0d  10276  nn0red  10277  suprzcl  10351  nn0zd  10375  zred  10377  zsupss  10567  rpnnen1lem1  10602  rpnnen1lem2  10603  rpred  10650  fzfi  11313  seqf1olem1  11364  expcl2lem  11395  m1expcl  11406  hashxrcl  11642  seqcoll2  11715  wrdeqcats1  11790  wrdind  11793  limsupgre  12277  rlimpm  12296  rlimclim  12342  isercolllem1  12460  isercolllem2  12461  isercoll  12463  iseraltlem2  12478  iseraltlem3  12479  fsumcvg3  12525  ackbijnn  12609  bitsval  12938  bitsfzolem  12948  bitsinv1  12956  smuval2  12996  gcdcllem3  13015  eulerthlem2  13173  prmdivdiv  13178  prmreclem1  13286  prmreclem2  13287  prmreclem3  13288  1arith  13297  4sqlem13  13327  4sqlem14  13328  4sqlem17  13331  vdwlem5  13355  vdwlem8  13358  vdwlem12  13362  vdwnnlem3  13367  ramtlecl  13370  ramcl2lem  13379  ramcl2  13386  ramxrcl  13387  submrc  13855  mreexexlem2d  13872  catlid  13910  catrid  13911  sscpwex  14017  subcrcl  14018  sscres  14025  wunfunc  14098  funcres2c  14100  cofull  14133  cofth  14134  coffth  14135  rescfth  14136  homarel  14193  arwrcl  14201  idaf  14220  homdmcoa  14224  coaval  14225  coapm  14228  catciso  14264  catcoppccl  14265  catcfuccl  14266  catcxpccl  14306  acsfiindd  14605  psssdm2  14649  submrcl  14749  gsumval2  14785  issubg  14946  isnsg  14971  nmzsubg  14983  conjnmz  15041  conjnmzb  15042  cntzsubm  15136  cntzsubg  15137  odlem2  15179  gexlem2  15218  sylow1lem2  15235  sylow1lem4  15237  sylow2a  15255  efglem  15350  efgtf  15356  efgtlen  15360  efgsres  15372  efgsfo  15373  efgredlemg  15376  efgredleme  15377  efgredlemd  15378  efgredlemc  15379  efgredlem  15381  efgred  15382  efgcpbllemb  15389  frgpuplem  15406  frgpnabllem2  15487  cyggex2  15508  dprdfsub  15581  dprdf11  15583  dprd2da  15602  ablfac2  15649  issubrg  15870  cntzsubr  15902  abvrcl  15911  lbsextlem3  16234  sralmod  16260  rrgeq0  16352  psrbagconf1o  16441  psrass1lem  16444  psrdi  16472  psrdir  16473  psrass23  16475  resspsrmul  16482  mplelf  16499  mplsubrglem  16504  mpladd  16507  mplmul  16508  mplvsca  16512  mplmonmul  16529  mplcoe2  16532  mplind  16564  psropprmul  16634  zlpirlem2  16771  zlpirlem3  16772  znf1o  16834  cygznlem2a  16850  ocvlss  16901  lsmcss  16921  isobs  16949  neiptoptop  17197  restbas  17224  ordtbas2  17257  ordtopn1  17260  ordtopn2  17261  ordtrest  17268  iocpnfordt  17281  icomnfordt  17282  lmrcl  17297  subbascn  17320  lmss  17364  cnconn  17487  clscon  17495  concompclo  17500  subislly  17546  cldllycmp  17560  kgeni  17571  llycmpkgen2  17584  1stckgenlem  17587  ptbasfi  17615  xkoopn  17623  txcls  17638  dfac14lem  17651  txcnp  17654  ptcnplem  17655  upxp  17657  txtube  17674  txcmplem1  17675  txcmplem2  17676  txkgen  17686  xkopt  17689  xkococnlem  17693  txcon  17723  basqtop  17745  tgqtop  17746  kqnrmlem1  17777  kqnrmlem2  17778  nrmhmph  17828  ptcmpfi  17847  elmptrab  17861  uzrest  17931  fclsfnflim  18061  flimfnfcls  18062  cnpfcf  18075  alexsubALTlem3  18082  alexsubALTlem4  18083  ptcmplem2  18086  ptcmplem5  18089  tsmsres  18175  restutop  18269  prdsxmetlem  18400  isxms2  18480  prdsbl  18523  met2ndci  18554  nmdvr  18708  nrginvrcnlem  18728  nrginvrcn  18729  tgqioo  18833  zdis  18849  reperflem  18851  reconnlem2  18860  reconn  18861  xrge0gsumle  18866  xrge0tsms  18867  xmetdcn  18871  metdcn  18873  metdscn2  18889  cncfmpt2ss  18947  icchmeo  18968  iccpnfcnv  18971  xrhmeo  18973  icccvx  18977  cnheibor  18982  bndth  18985  evth  18986  lebnum  18991  isphtpc  19021  reparphti  19024  pcoass  19051  nmoleub2lem  19124  nmoleub2lem3  19125  nmoleub2lem2  19126  nmoleub3  19129  nmhmcn  19130  cfili  19223  cfilfcls  19229  caussi  19252  equivcau  19255  minveclem4b  19334  minveclem4  19335  evthicc2  19359  ovolfcl  19365  ovolfioo  19366  ovolficc  19367  ovolficcss  19368  ovolfsval  19369  ovolmge0  19375  ovollb2lem  19386  ovolunlem1a  19394  ovoliunlem1  19400  ovolicc1  19414  ovolicc2lem4  19418  ovolicc2lem5  19419  ioombl1lem2  19455  ioombl1lem4  19457  ovolfs2  19465  ioorcl  19471  uniiccdif  19472  uniioovol  19473  uniiccvol  19474  uniioombllem2a  19476  uniioombllem2  19477  uniioombllem3a  19478  uniioombllem3  19479  uniioombllem4  19480  uniioombllem5  19481  uniioombllem6  19482  dyadmbl  19494  volsup2  19499  volivth  19501  vitalilem1  19502  vitalilem2  19503  vitalilem4  19505  mbfimaopnlem  19549  cncombf  19552  cnmbf  19553  mbflimsup  19560  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  itg2const2  19635  itg2lea  19638  itg2eqa  19639  itg2split  19643  itg2i1fseq  19649  itg2gt0  19654  limcco  19782  dvcl  19788  perfdvf  19792  dvreslem  19798  dvres2lem  19799  dvidlem  19804  dvcnp2  19808  dvmulbr  19827  dvferm1lem  19870  dvferm2lem  19872  dvferm  19874  rolle  19876  dvlipcn  19880  dvlip2  19881  c1liplem1  19882  c1lip2  19884  dvgt0lem1  19888  dvivthlem1  19894  dvivth  19896  lhop1lem  19899  lhop1  19900  lhop2  19901  lhop  19902  dvfsumlem1  19912  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlimge0  19916  dvfsumrlim  19917  dvfsumrlim2  19918  dvfsum2  19920  ftc1lem5  19926  ftc1lem6  19927  itgsubstlem  19934  itgsubst  19935  mdegleb  19989  mdegaddle  19999  mdegvsca  20001  mdegmullem  20003  ig1peu  20096  plybss  20115  plyaddcl  20141  plymulcl  20142  plysubcl  20143  coeidlem  20158  coesub  20177  dgrmulc  20191  dgrcolem1  20193  dgrcolem2  20194  dgrco  20195  quotlem  20219  quotcl2  20221  quotdgr  20222  plyrem  20224  facth  20225  quotcan  20228  vieta1lem1  20229  vieta1  20231  elqaalem3  20240  aalioulem2  20252  aalioulem3  20253  taylfvallem1  20275  tayl0  20280  dvntaylp  20289  taylthlem1  20291  taylthlem2  20292  radcnvlt1  20336  radcnvle  20338  pserulm  20340  psercnlem2  20342  psercnlem1  20343  psercn  20344  pserdvlem1  20345  pserdvlem2  20346  abelthlem3  20351  abelthlem5  20353  abelthlem6  20354  abelth  20359  efcvx  20367  tanord  20442  tanregt0  20443  efif1olem4  20449  logtayl  20553  logccv  20556  cxpcn3  20634  ssscongptld  20668  chordthmlem  20675  chordthmlem4  20678  chordthmlem5  20679  chordthm  20680  asinrecl  20744  atantan  20765  dvatan  20777  leibpi  20784  rlimcnp  20806  efrlim  20810  cvxcl  20825  scvxcvx  20826  jensenlem1  20827  jensenlem2  20828  jensen  20829  amgmlem  20830  harmonicbnd3  20848  wilthlem1  20853  ftalem3  20859  ftalem5  20861  ftalem7  20863  basellem3  20867  basellem4  20868  basellem5  20869  ppisval  20888  chtf  20893  efchtcl  20896  chtge0  20897  sgmval2  20928  ppinprm  20937  chtprm  20938  chtnprm  20939  chtwordi  20941  chtdif  20943  efchtdvds  20944  sqff1o  20967  fsumdvdsdiaglem  20970  fsumdvdsdiag  20971  fsumdvdscom  20972  musum  20978  muinv  20980  dvdsmulf1o  20981  sgmmul  20987  chtlepsi  20992  chtleppi  20996  pclogsum  21001  chpval2  21004  chpchtsum  21005  chpub  21006  perfectlem2  21016  dchrelbasd  21025  dchrrcl  21026  dchrzrh1  21030  dchrzrhmul  21032  dchrinvcl  21039  dchrfi  21041  dchrghm  21042  dchr1  21043  dchrabs  21046  dchrinv  21047  dchrptlem2  21051  dchrsum2  21054  sumdchr2  21056  sum2dchr  21060  lgscl  21096  lgsquadlem1  21140  lgsquadlem2  21141  2sqlem6  21155  2sqlem8  21158  2sqlem9  21159  chebbnd1lem1  21165  chtppilimlem1  21169  rplogsumlem2  21181  dchrisum0flblem1  21204  rpvmasum2  21208  dchrisum0re  21209  dchrisum0lema  21210  dchrisum0lem1b  21211  dchrisum0lem1  21212  dchrisum0lem2a  21213  dchrisum0lem2  21214  dchrisum0lem3  21215  dchrisum0  21216  rplogsum  21223  dirith2  21224  mudivsum  21226  mulogsum  21228  mulog2sumlem2  21231  vmalogdivsum2  21234  logsqvma  21238  logsqvma2  21239  selberglem3  21243  selberg  21244  chpdifbndlem1  21249  selberg34r  21267  pntsval2  21272  pntrlog2bndlem1  21273  pntpbnd1a  21281  pntpbnd1  21282  pntpbnd2  21283  pntibndlem2a  21286  pntibndlem2  21287  pntibndlem3  21288  pntlemd  21290  padicabv  21326  umgrass  21356  umgran0  21357  usgrass  21386  redwlk  21608  issubgo  21893  nvvop  22090  nmcnc  22194  ubthlem1  22374  minvecolem2  22379  minvecolem3  22380  minvecolem5  22385  minvecolem6  22386  minvecolem7  22387  hlimcaui  22741  pjocini  23202  eliccelico  24142  elicoelioo  24143  iundisjfi  24154  iundisj2fi  24155  divnumden2  24163  xrsmulgzz  24202  ressmulgnn  24207  ressmulgnn0  24208  xrge0addass  24213  xrge0addgt0  24216  xrge0adddir  24217  xrge0npcan  24218  fsumrp0cl  24219  xrge0tsmsd  24225  dvrdir  24228  rdivmuldivd  24229  dvrcan5  24231  elrhmunit  24260  rhmunitinv  24262  cnre2csqima  24311  tpr2rico  24312  cnvordtrestixx  24313  xrge0iifcnv  24321  xrge0iifhom  24325  xrge0mulc1cn  24329  rge0scvg  24337  lmxrge0  24339  cnzh  24356  rezh  24357  qqhval2  24368  qqhvq  24373  qqhnm  24376  qqhcn  24377  qqhucn  24378  indsum  24422  indf1ofs  24425  esumel  24444  esumle  24451  esummono  24452  gsumesum  24453  esumlub  24454  esumlef  24456  esumcst  24457  esumfzf  24461  esumfsup  24462  esumfsupre  24463  esumpinfval  24465  esumpfinvallem  24466  esumpfinval  24467  esumpfinvalf  24468  esumpinfsum  24469  esumpcvgval  24470  esumpmono  24471  esummulc1  24473  esummulc2  24474  esumdivc  24475  hasheuni  24477  esumcvg  24478  sigainb  24521  measun  24567  measunl  24572  measiun  24574  meascnbl  24575  voliune  24587  volfiniune  24588  dya2icoseg2  24630  dya2iocnrect  24633  sxbrsigalem2  24638  sibfof  24656  probun  24679  probdif  24680  probvalrnd  24684  probmeasb  24690  cndprobin  24694  bayesth  24699  ballotlemsdom  24771  ballotlemrv2  24781  ballotlemfrci  24787  lgamgulmlem2  24816  lgamcvg2  24841  subfacp1lem5  24872  erdszelem4  24882  erdszelem6  24884  erdszelem7  24885  erdszelem8  24886  erdszelem9  24887  conpcon  24924  cvxscon  24932  rescon  24935  iccllyscon  24939  rellyscon  24940  cvmsrcl  24953  cvmliftmolem2  24971  cvmlift2lem12  25003  cvmlift3  25017  snmlval  25020  clim2prod  25218  ntrivcvg  25227  ntrivcvgfvn0  25229  ntrivcvgtail  25230  ntrivcvgmullem  25231  ntrivcvgmul  25232  prodrblem  25257  prodmolem2a  25262  axlowdimlem16  25898  axcontlem10  25914  mblfinlem2  26246  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  ftc1cnnclem  26280  ftc1anclem6  26287  islocfin  26378  neibastop1  26390  fdc  26451  prdsbnd  26504  ismtyval  26511  heiborlem3  26524  heiborlem5  26526  heiborlem10  26531  rrnequiv  26546  eldiophb  26817  4rexfrabdioph  26860  6rexfrabdioph  26861  diophren  26876  rencldnfilem  26883  pellexlem3  26896  pellfundglb  26950  rmxypairf1o  26976  rmxycomplete  26982  rmxyneg  26985  rmxyadd  26986  rmxy1  26987  rmxy0  26988  monotuz  27006  jm2.22  27068  aomclem2  27132  isnumbasgrp  27251  dfacbasgrp  27252  hbtlem2  27307  hbt  27313  elmnc  27320  symggen  27390  symgtrinv  27392  psgnunilem5  27396  psgnunilem2  27397  psgnuni  27401  issdrg  27484  cntzsdrg  27489  mon1psubm  27504  stoweidlem26  27753  stoweidlem51  27778  lswrdcshw  28288  suctrALT3  29098  chordthmALT  29107  iunconlem2  29109  bnj1213  29232  bnj1417  29472  osumcllem7N  30821  pexmidlem4N  30832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator