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  4623  suctr  4668  sofld  5321  fvrn0  5756  elmpt2cl  6291  ofrval  6318  mpt2xopn0yelv  6467  mpt2xopxnop0  6469  tpostpos  6502  opiota  6538  riotacl  6567  riotasbc  6568  smores  6617  tz7.44-2  6668  omopthlem2  6902  f1opwfi  7413  supub  7467  suplub  7468  ordtypelem3  7492  ordtypelem4  7493  ordtypelem6  7495  ordtypelem7  7496  wemapso2lem  7522  wemapso2  7524  unxpwdom2  7559  cantnfres  7636  wemapwe  7657  oef1o  7658  cnfcomlem  7659  r1pwss  7713  r1elwf  7725  rankr1ai  7727  r0weon  7899  infxpenlem  7900  acnlem  7934  acndom2  7940  infpwfien  7948  alephfp  7994  ackbij1b  8124  cflim2  8148  fin23lem26  8210  isf32lem5  8242  isf32lem7  8244  isf32lem8  8245  isf32lem9  8246  isfin1-3  8271  fin1a2lem9  8293  fin1a2lem11  8295  hsmexlem5  8315  zorn2lem3  8383  zorn2lem4  8384  zorn2lem5  8385  ttukeylem6  8399  ttukeylem7  8400  iundom2g  8420  fpwwe2lem12  8521  pwfseqlem3  8540  gch2  8555  wunom  8600  rexrd  9139  nnred  10020  nncnd  10021  un0addcl  10258  un0mulcl  10259  nnnn0d  10279  nn0red  10280  suprzcl  10354  nn0zd  10378  zred  10380  zsupss  10570  rpnnen1lem1  10605  rpnnen1lem2  10606  rpred  10653  fzfi  11316  seqf1olem1  11367  expcl2lem  11398  m1expcl  11409  hashxrcl  11645  seqcoll2  11718  wrdeqcats1  11793  wrdind  11796  limsupgre  12280  rlimpm  12299  rlimclim  12345  isercolllem1  12463  isercolllem2  12464  isercoll  12466  iseraltlem2  12481  iseraltlem3  12482  fsumcvg3  12528  ackbijnn  12612  bitsval  12941  bitsfzolem  12951  bitsinv1  12959  smuval2  12999  gcdcllem3  13018  eulerthlem2  13176  prmdivdiv  13181  prmreclem1  13289  prmreclem2  13290  prmreclem3  13291  1arith  13300  4sqlem13  13330  4sqlem14  13331  4sqlem17  13334  vdwlem5  13358  vdwlem8  13361  vdwlem12  13365  vdwnnlem3  13370  ramtlecl  13373  ramcl2lem  13382  ramcl2  13389  ramxrcl  13390  submrc  13858  mreexexlem2d  13875  catlid  13913  catrid  13914  sscpwex  14020  subcrcl  14021  sscres  14028  wunfunc  14101  funcres2c  14103  cofull  14136  cofth  14137  coffth  14138  rescfth  14139  homarel  14196  arwrcl  14204  idaf  14223  homdmcoa  14227  coaval  14228  coapm  14231  catciso  14267  catcoppccl  14268  catcfuccl  14269  catcxpccl  14309  acsfiindd  14608  psssdm2  14652  submrcl  14752  gsumval2  14788  issubg  14949  isnsg  14974  nmzsubg  14986  conjnmz  15044  conjnmzb  15045  cntzsubm  15139  cntzsubg  15140  odlem2  15182  gexlem2  15221  sylow1lem2  15238  sylow1lem4  15240  sylow2a  15258  efglem  15353  efgtf  15359  efgtlen  15363  efgsres  15375  efgsfo  15376  efgredlemg  15379  efgredleme  15380  efgredlemd  15381  efgredlemc  15382  efgredlem  15384  efgred  15385  efgcpbllemb  15392  frgpuplem  15409  frgpnabllem2  15490  cyggex2  15511  dprdfsub  15584  dprdf11  15586  dprd2da  15605  ablfac2  15652  issubrg  15873  cntzsubr  15905  abvrcl  15914  lbsextlem3  16237  sralmod  16263  rrgeq0  16355  psrbagconf1o  16444  psrass1lem  16447  psrdi  16475  psrdir  16476  psrass23  16478  resspsrmul  16485  mplelf  16502  mplsubrglem  16507  mpladd  16510  mplmul  16511  mplvsca  16515  mplmonmul  16532  mplcoe2  16535  mplind  16567  psropprmul  16637  zlpirlem2  16774  zlpirlem3  16775  znf1o  16837  cygznlem2a  16853  ocvlss  16904  lsmcss  16924  isobs  16952  neiptoptop  17200  restbas  17227  ordtbas2  17260  ordtopn1  17263  ordtopn2  17264  ordtrest  17271  iocpnfordt  17284  icomnfordt  17285  lmrcl  17300  subbascn  17323  lmss  17367  cnconn  17490  clscon  17498  concompclo  17503  subislly  17549  cldllycmp  17563  kgeni  17574  llycmpkgen2  17587  1stckgenlem  17590  ptbasfi  17618  xkoopn  17626  txcls  17641  dfac14lem  17654  txcnp  17657  ptcnplem  17658  upxp  17660  txtube  17677  txcmplem1  17678  txcmplem2  17679  txkgen  17689  xkopt  17692  xkococnlem  17696  txcon  17726  basqtop  17748  tgqtop  17749  kqnrmlem1  17780  kqnrmlem2  17781  nrmhmph  17831  ptcmpfi  17850  elmptrab  17864  uzrest  17934  fclsfnflim  18064  flimfnfcls  18065  cnpfcf  18078  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem2  18089  ptcmplem5  18092  tsmsres  18178  restutop  18272  prdsxmetlem  18403  isxms2  18483  prdsbl  18526  met2ndci  18557  nmdvr  18711  nrginvrcnlem  18731  nrginvrcn  18732  tgqioo  18836  zdis  18852  reperflem  18854  reconnlem2  18863  reconn  18864  xrge0gsumle  18869  xrge0tsms  18870  xmetdcn  18874  metdcn  18876  metdscn2  18892  cncfmpt2ss  18950  icchmeo  18971  iccpnfcnv  18974  xrhmeo  18976  icccvx  18980  cnheibor  18985  bndth  18988  evth  18989  lebnum  18994  isphtpc  19024  reparphti  19027  pcoass  19054  nmoleub2lem  19127  nmoleub2lem3  19128  nmoleub2lem2  19129  nmoleub3  19132  nmhmcn  19133  cfili  19226  cfilfcls  19232  caussi  19255  equivcau  19258  minveclem4b  19337  minveclem4  19338  evthicc2  19362  ovolfcl  19368  ovolfioo  19369  ovolficc  19370  ovolficcss  19371  ovolfsval  19372  ovolmge0  19378  ovollb2lem  19389  ovolunlem1a  19397  ovoliunlem1  19403  ovolicc1  19417  ovolicc2lem4  19421  ovolicc2lem5  19422  ioombl1lem2  19458  ioombl1lem4  19460  ovolfs2  19468  ioorcl  19474  uniiccdif  19475  uniioovol  19476  uniiccvol  19477  uniioombllem2a  19479  uniioombllem2  19480  uniioombllem3a  19481  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  uniioombllem6  19485  dyadmbl  19497  volsup2  19502  volivth  19504  vitalilem1  19505  vitalilem2  19506  vitalilem4  19508  mbfimaopnlem  19550  cncombf  19553  cnmbf  19554  mbflimsup  19561  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  itg2const2  19636  itg2lea  19639  itg2eqa  19640  itg2split  19644  itg2i1fseq  19650  itg2gt0  19655  limcco  19785  dvcl  19791  perfdvf  19795  dvreslem  19801  dvres2lem  19802  dvidlem  19807  dvcnp2  19811  dvmulbr  19830  dvferm1lem  19873  dvferm2lem  19875  dvferm  19877  rolle  19879  dvlipcn  19883  dvlip2  19884  c1liplem1  19885  c1lip2  19887  dvgt0lem1  19891  dvivthlem1  19897  dvivth  19899  lhop1lem  19902  lhop1  19903  lhop2  19904  lhop  19905  dvfsumlem1  19915  dvfsumlem2  19916  dvfsumlem3  19917  dvfsumlem4  19918  dvfsumrlimge0  19919  dvfsumrlim  19920  dvfsumrlim2  19921  dvfsum2  19923  ftc1lem5  19929  ftc1lem6  19930  itgsubstlem  19937  itgsubst  19938  mdegleb  19992  mdegaddle  20002  mdegvsca  20004  mdegmullem  20006  ig1peu  20099  plybss  20118  plyaddcl  20144  plymulcl  20145  plysubcl  20146  coeidlem  20161  coesub  20180  dgrmulc  20194  dgrcolem1  20196  dgrcolem2  20197  dgrco  20198  quotlem  20222  quotcl2  20224  quotdgr  20225  plyrem  20227  facth  20228  quotcan  20231  vieta1lem1  20232  vieta1  20234  elqaalem3  20243  aalioulem2  20255  aalioulem3  20256  taylfvallem1  20278  tayl0  20283  dvntaylp  20292  taylthlem1  20294  taylthlem2  20295  radcnvlt1  20339  radcnvle  20341  pserulm  20343  psercnlem2  20345  psercnlem1  20346  psercn  20347  pserdvlem1  20348  pserdvlem2  20349  abelthlem3  20354  abelthlem5  20356  abelthlem6  20357  abelth  20362  efcvx  20370  tanord  20445  tanregt0  20446  efif1olem4  20452  logtayl  20556  logccv  20559  cxpcn3  20637  ssscongptld  20671  chordthmlem  20678  chordthmlem4  20681  chordthmlem5  20682  chordthm  20683  asinrecl  20747  atantan  20768  dvatan  20780  leibpi  20787  rlimcnp  20809  efrlim  20813  cvxcl  20828  scvxcvx  20829  jensenlem1  20830  jensenlem2  20831  jensen  20832  amgmlem  20833  harmonicbnd3  20851  wilthlem1  20856  ftalem3  20862  ftalem5  20864  ftalem7  20866  basellem3  20870  basellem4  20871  basellem5  20872  ppisval  20891  chtf  20896  efchtcl  20899  chtge0  20900  sgmval2  20931  ppinprm  20940  chtprm  20941  chtnprm  20942  chtwordi  20944  chtdif  20946  efchtdvds  20947  sqff1o  20970  fsumdvdsdiaglem  20973  fsumdvdsdiag  20974  fsumdvdscom  20975  musum  20981  muinv  20983  dvdsmulf1o  20984  sgmmul  20990  chtlepsi  20995  chtleppi  20999  pclogsum  21004  chpval2  21007  chpchtsum  21008  chpub  21009  perfectlem2  21019  dchrelbasd  21028  dchrrcl  21029  dchrzrh1  21033  dchrzrhmul  21035  dchrinvcl  21042  dchrfi  21044  dchrghm  21045  dchr1  21046  dchrabs  21049  dchrinv  21050  dchrptlem2  21054  dchrsum2  21057  sumdchr2  21059  sum2dchr  21063  lgscl  21099  lgsquadlem1  21143  lgsquadlem2  21144  2sqlem6  21158  2sqlem8  21161  2sqlem9  21162  chebbnd1lem1  21168  chtppilimlem1  21172  rplogsumlem2  21184  dchrisum0flblem1  21207  rpvmasum2  21211  dchrisum0re  21212  dchrisum0lema  21213  dchrisum0lem1b  21214  dchrisum0lem1  21215  dchrisum0lem2a  21216  dchrisum0lem2  21217  dchrisum0lem3  21218  dchrisum0  21219  rplogsum  21226  dirith2  21227  mudivsum  21229  mulogsum  21231  mulog2sumlem2  21234  vmalogdivsum2  21237  logsqvma  21241  logsqvma2  21242  selberglem3  21246  selberg  21247  chpdifbndlem1  21252  selberg34r  21270  pntsval2  21275  pntrlog2bndlem1  21276  pntpbnd1a  21284  pntpbnd1  21285  pntpbnd2  21286  pntibndlem2a  21289  pntibndlem2  21290  pntibndlem3  21291  pntlemd  21293  padicabv  21329  umgrass  21359  umgran0  21360  usgrass  21389  redwlk  21611  issubgo  21896  nvvop  22093  nmcnc  22197  ubthlem1  22377  minvecolem2  22382  minvecolem3  22383  minvecolem5  22388  minvecolem6  22389  minvecolem7  22390  hlimcaui  22744  pjocini  23205  eliccelico  24145  elicoelioo  24146  iundisjfi  24157  iundisj2fi  24158  divnumden2  24166  xrsmulgzz  24205  ressmulgnn  24210  ressmulgnn0  24211  xrge0addass  24216  xrge0addgt0  24219  xrge0adddir  24220  xrge0npcan  24221  fsumrp0cl  24222  xrge0tsmsd  24228  dvrdir  24231  rdivmuldivd  24232  dvrcan5  24234  elrhmunit  24263  rhmunitinv  24265  cnre2csqima  24314  tpr2rico  24315  cnvordtrestixx  24316  xrge0iifcnv  24324  xrge0iifhom  24328  xrge0mulc1cn  24332  rge0scvg  24340  lmxrge0  24342  cnzh  24359  rezh  24360  qqhval2  24371  qqhvq  24376  qqhnm  24379  qqhcn  24380  qqhucn  24381  indsum  24425  indf1ofs  24428  esumel  24447  esumle  24454  esummono  24455  gsumesum  24456  esumlub  24457  esumlef  24459  esumcst  24460  esumfzf  24464  esumfsup  24465  esumfsupre  24466  esumpinfval  24468  esumpfinvallem  24469  esumpfinval  24470  esumpfinvalf  24471  esumpinfsum  24472  esumpcvgval  24473  esumpmono  24474  esummulc1  24476  esummulc2  24477  esumdivc  24478  hasheuni  24480  esumcvg  24481  sigainb  24524  measun  24570  measunl  24575  measiun  24577  meascnbl  24578  voliune  24590  volfiniune  24591  dya2icoseg2  24633  dya2iocnrect  24636  sxbrsigalem2  24641  sibfof  24659  probun  24682  probdif  24683  probvalrnd  24687  probmeasb  24693  cndprobin  24697  bayesth  24702  ballotlemsdom  24774  ballotlemrv2  24784  ballotlemfrci  24790  lgamgulmlem2  24819  lgamcvg2  24844  subfacp1lem5  24875  erdszelem4  24885  erdszelem6  24887  erdszelem7  24888  erdszelem8  24889  erdszelem9  24890  conpcon  24927  cvxscon  24935  rescon  24938  iccllyscon  24942  rellyscon  24943  cvmsrcl  24956  cvmliftmolem2  24974  cvmlift2lem12  25006  cvmlift3  25020  snmlval  25023  clim2prod  25221  ntrivcvg  25230  ntrivcvgfvn0  25232  ntrivcvgtail  25233  ntrivcvgmullem  25234  ntrivcvgmul  25235  prodrblem  25260  prodmolem2a  25265  axlowdimlem16  25901  axcontlem10  25917  mblfinlem2  26256  itg2addnclem3  26272  itg2addnc  26273  itg2gt0cn  26274  ftc1cnnclem  26292  ftc1anclem6  26299  islocfin  26390  neibastop1  26402  fdc  26463  prdsbnd  26516  ismtyval  26523  heiborlem3  26536  heiborlem5  26538  heiborlem10  26543  rrnequiv  26558  eldiophb  26829  4rexfrabdioph  26872  6rexfrabdioph  26873  diophren  26888  rencldnfilem  26895  pellexlem3  26908  pellfundglb  26962  rmxypairf1o  26988  rmxycomplete  26994  rmxyneg  26997  rmxyadd  26998  rmxy1  26999  rmxy0  27000  monotuz  27018  jm2.22  27080  aomclem2  27144  isnumbasgrp  27263  dfacbasgrp  27264  hbtlem2  27319  hbt  27325  elmnc  27332  symggen  27402  symgtrinv  27404  psgnunilem5  27408  psgnunilem2  27409  psgnuni  27413  issdrg  27496  cntzsdrg  27501  mon1psubm  27516  stoweidlem26  27765  stoweidlem51  27790  lswrdcshw  28300  suctrALT3  29110  chordthmALT  29119  iunconlem2  29121  bnj1213  29244  bnj1417  29484  osumcllem7N  30833  pexmidlem4N  30844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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