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

Theorem sseldi 3338
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 3336 . 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 1725    C_ wss 3312
This theorem is referenced by:  onfr  4612  suctr  4657  sofld  5310  fvrn0  5745  elmpt2cl  6280  ofrval  6307  mpt2xopn0yelv  6456  mpt2xopxnop0  6458  tpostpos  6491  opiota  6527  riotacl  6556  riotasbc  6557  smores  6606  tz7.44-2  6657  omopthlem2  6891  f1opwfi  7402  supub  7456  suplub  7457  ordtypelem3  7481  ordtypelem4  7482  ordtypelem6  7484  ordtypelem7  7485  wemapso2lem  7511  wemapso2  7513  unxpwdom2  7548  cantnfres  7625  wemapwe  7646  oef1o  7647  cnfcomlem  7648  r1pwss  7702  r1elwf  7714  rankr1ai  7716  r0weon  7886  infxpenlem  7887  acnlem  7921  acndom2  7927  infpwfien  7935  alephfp  7981  ackbij1b  8111  cflim2  8135  fin23lem26  8197  isf32lem5  8229  isf32lem7  8231  isf32lem8  8232  isf32lem9  8233  isfin1-3  8258  fin1a2lem9  8280  fin1a2lem11  8282  hsmexlem5  8302  zorn2lem3  8370  zorn2lem4  8371  zorn2lem5  8372  ttukeylem6  8386  ttukeylem7  8387  iundom2g  8407  fpwwe2lem12  8508  pwfseqlem3  8527  gch2  8546  wunom  8587  rexrd  9126  nnred  10007  nncnd  10008  un0addcl  10245  un0mulcl  10246  nnnn0d  10266  nn0red  10267  suprzcl  10341  nn0zd  10365  zred  10367  zsupss  10557  rpnnen1lem1  10592  rpnnen1lem2  10593  rpred  10640  fzfi  11303  seqf1olem1  11354  expcl2lem  11385  m1expcl  11396  hashxrcl  11632  seqcoll2  11705  wrdeqcats1  11780  wrdind  11783  limsupgre  12267  rlimpm  12286  rlimclim  12332  isercolllem1  12450  isercolllem2  12451  isercoll  12453  iseraltlem2  12468  iseraltlem3  12469  fsumcvg3  12515  ackbijnn  12599  bitsval  12928  bitsfzolem  12938  bitsinv1  12946  smuval2  12986  gcdcllem3  13005  eulerthlem2  13163  prmdivdiv  13168  prmreclem1  13276  prmreclem2  13277  prmreclem3  13278  1arith  13287  4sqlem13  13317  4sqlem14  13318  4sqlem17  13321  vdwlem5  13345  vdwlem8  13348  vdwlem12  13352  vdwnnlem3  13357  ramtlecl  13360  ramcl2lem  13369  ramcl2  13376  ramxrcl  13377  submrc  13845  mreexexlem2d  13862  catlid  13900  catrid  13901  sscpwex  14007  subcrcl  14008  sscres  14015  wunfunc  14088  funcres2c  14090  cofull  14123  cofth  14124  coffth  14125  rescfth  14126  homarel  14183  arwrcl  14191  idaf  14210  homdmcoa  14214  coaval  14215  coapm  14218  catciso  14254  catcoppccl  14255  catcfuccl  14256  catcxpccl  14296  acsfiindd  14595  psssdm2  14639  submrcl  14739  gsumval2  14775  issubg  14936  isnsg  14961  nmzsubg  14973  conjnmz  15031  conjnmzb  15032  cntzsubm  15126  cntzsubg  15127  odlem2  15169  gexlem2  15208  sylow1lem2  15225  sylow1lem4  15227  sylow2a  15245  efglem  15340  efgtf  15346  efgtlen  15350  efgsres  15362  efgsfo  15363  efgredlemg  15366  efgredleme  15367  efgredlemd  15368  efgredlemc  15369  efgredlem  15371  efgred  15372  efgcpbllemb  15379  frgpuplem  15396  frgpnabllem2  15477  cyggex2  15498  dprdfsub  15571  dprdf11  15573  dprd2da  15592  ablfac2  15639  issubrg  15860  cntzsubr  15892  abvrcl  15901  lbsextlem3  16224  sralmod  16250  rrgeq0  16342  psrbagconf1o  16431  psrass1lem  16434  psrdi  16462  psrdir  16463  psrass23  16465  resspsrmul  16472  mplelf  16489  mplsubrglem  16494  mpladd  16497  mplmul  16498  mplvsca  16502  mplmonmul  16519  mplcoe2  16522  mplind  16554  psropprmul  16624  zlpirlem2  16761  zlpirlem3  16762  znf1o  16824  cygznlem2a  16840  ocvlss  16891  lsmcss  16911  isobs  16939  neiptoptop  17187  restbas  17214  ordtbas2  17247  ordtopn1  17250  ordtopn2  17251  ordtrest  17258  iocpnfordt  17271  icomnfordt  17272  lmrcl  17287  subbascn  17310  lmss  17354  cnconn  17477  clscon  17485  concompclo  17490  subislly  17536  cldllycmp  17550  kgeni  17561  llycmpkgen2  17574  1stckgenlem  17577  ptbasfi  17605  xkoopn  17613  txcls  17628  dfac14lem  17641  txcnp  17644  ptcnplem  17645  upxp  17647  txtube  17664  txcmplem1  17665  txcmplem2  17666  txkgen  17676  xkopt  17679  xkococnlem  17683  txcon  17713  basqtop  17735  tgqtop  17736  kqnrmlem1  17767  kqnrmlem2  17768  nrmhmph  17818  ptcmpfi  17837  elmptrab  17851  uzrest  17921  fclsfnflim  18051  flimfnfcls  18052  cnpfcf  18065  alexsubALTlem3  18072  alexsubALTlem4  18073  ptcmplem2  18076  ptcmplem5  18079  tsmsres  18165  restutop  18259  prdsxmetlem  18390  isxms2  18470  prdsbl  18513  met2ndci  18544  nmdvr  18698  nrginvrcnlem  18718  nrginvrcn  18719  tgqioo  18823  zdis  18839  reperflem  18841  reconnlem2  18850  reconn  18851  xrge0gsumle  18856  xrge0tsms  18857  xmetdcn  18861  metdcn  18863  metdscn2  18879  cncfmpt2ss  18937  icchmeo  18958  iccpnfcnv  18961  xrhmeo  18963  icccvx  18967  cnheibor  18972  bndth  18975  evth  18976  lebnum  18981  isphtpc  19011  reparphti  19014  pcoass  19041  nmoleub2lem  19114  nmoleub2lem3  19115  nmoleub2lem2  19116  nmoleub3  19119  nmhmcn  19120  cfili  19213  cfilfcls  19219  caussi  19242  equivcau  19245  minveclem4b  19324  minveclem4  19325  evthicc2  19349  ovolfcl  19355  ovolfioo  19356  ovolficc  19357  ovolficcss  19358  ovolfsval  19359  ovolmge0  19365  ovollb2lem  19376  ovolunlem1a  19384  ovoliunlem1  19390  ovolicc1  19404  ovolicc2lem4  19408  ovolicc2lem5  19409  ioombl1lem2  19445  ioombl1lem4  19447  ovolfs2  19455  ioorcl  19461  uniiccdif  19462  uniioovol  19463  uniiccvol  19464  uniioombllem2a  19466  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombllem6  19472  dyadmbl  19484  volsup2  19489  volivth  19491  vitalilem1  19492  vitalilem2  19493  vitalilem4  19495  mbfimaopnlem  19539  cncombf  19542  cnmbf  19543  mbflimsup  19550  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  itg2const2  19625  itg2lea  19628  itg2eqa  19629  itg2split  19633  itg2i1fseq  19639  itg2gt0  19644  limcco  19772  dvcl  19778  perfdvf  19782  dvreslem  19788  dvres2lem  19789  dvidlem  19794  dvcnp2  19798  dvmulbr  19817  dvferm1lem  19860  dvferm2lem  19862  dvferm  19864  rolle  19866  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  c1lip2  19874  dvgt0lem1  19878  dvivthlem1  19884  dvivth  19886  lhop1lem  19889  lhop1  19890  lhop2  19891  lhop  19892  dvfsumlem1  19902  dvfsumlem2  19903  dvfsumlem3  19904  dvfsumlem4  19905  dvfsumrlimge0  19906  dvfsumrlim  19907  dvfsumrlim2  19908  dvfsum2  19910  ftc1lem5  19916  ftc1lem6  19917  itgsubstlem  19924  itgsubst  19925  mdegleb  19979  mdegaddle  19989  mdegvsca  19991  mdegmullem  19993  ig1peu  20086  plybss  20105  plyaddcl  20131  plymulcl  20132  plysubcl  20133  coeidlem  20148  coesub  20167  dgrmulc  20181  dgrcolem1  20183  dgrcolem2  20184  dgrco  20185  quotlem  20209  quotcl2  20211  quotdgr  20212  plyrem  20214  facth  20215  quotcan  20218  vieta1lem1  20219  vieta1  20221  elqaalem3  20230  aalioulem2  20242  aalioulem3  20243  taylfvallem1  20265  tayl0  20270  dvntaylp  20279  taylthlem1  20281  taylthlem2  20282  radcnvlt1  20326  radcnvle  20328  pserulm  20330  psercnlem2  20332  psercnlem1  20333  psercn  20334  pserdvlem1  20335  pserdvlem2  20336  abelthlem3  20341  abelthlem5  20343  abelthlem6  20344  abelth  20349  efcvx  20357  tanord  20432  tanregt0  20433  efif1olem4  20439  logtayl  20543  logccv  20546  cxpcn3  20624  ssscongptld  20658  chordthmlem  20665  chordthmlem4  20668  chordthmlem5  20669  chordthm  20670  asinrecl  20734  atantan  20755  dvatan  20767  leibpi  20774  rlimcnp  20796  efrlim  20800  cvxcl  20815  scvxcvx  20816  jensenlem1  20817  jensenlem2  20818  jensen  20819  amgmlem  20820  harmonicbnd3  20838  wilthlem1  20843  ftalem3  20849  ftalem5  20851  ftalem7  20853  basellem3  20857  basellem4  20858  basellem5  20859  ppisval  20878  chtf  20883  efchtcl  20886  chtge0  20887  sgmval2  20918  ppinprm  20927  chtprm  20928  chtnprm  20929  chtwordi  20931  chtdif  20933  efchtdvds  20934  sqff1o  20957  fsumdvdsdiaglem  20960  fsumdvdsdiag  20961  fsumdvdscom  20962  musum  20968  muinv  20970  dvdsmulf1o  20971  sgmmul  20977  chtlepsi  20982  chtleppi  20986  pclogsum  20991  chpval2  20994  chpchtsum  20995  chpub  20996  perfectlem2  21006  dchrelbasd  21015  dchrrcl  21016  dchrzrh1  21020  dchrzrhmul  21022  dchrinvcl  21029  dchrfi  21031  dchrghm  21032  dchr1  21033  dchrabs  21036  dchrinv  21037  dchrptlem2  21041  dchrsum2  21044  sumdchr2  21046  sum2dchr  21050  lgscl  21086  lgsquadlem1  21130  lgsquadlem2  21131  2sqlem6  21145  2sqlem8  21148  2sqlem9  21149  chebbnd1lem1  21155  chtppilimlem1  21159  rplogsumlem2  21171  dchrisum0flblem1  21194  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lema  21200  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  dchrisum0  21206  rplogsum  21213  dirith2  21214  mudivsum  21216  mulogsum  21218  mulog2sumlem2  21221  vmalogdivsum2  21224  logsqvma  21228  logsqvma2  21229  selberglem3  21233  selberg  21234  chpdifbndlem1  21239  selberg34r  21257  pntsval2  21262  pntrlog2bndlem1  21263  pntpbnd1a  21271  pntpbnd1  21272  pntpbnd2  21273  pntibndlem2a  21276  pntibndlem2  21277  pntibndlem3  21278  pntlemd  21280  padicabv  21316  umgrass  21346  umgran0  21347  usgrass  21376  redwlk  21598  issubgo  21883  nvvop  22080  nmcnc  22184  ubthlem1  22364  minvecolem2  22369  minvecolem3  22370  minvecolem5  22375  minvecolem6  22376  minvecolem7  22377  hlimcaui  22731  pjocini  23192  eliccelico  24132  elicoelioo  24133  iundisjfi  24144  iundisj2fi  24145  divnumden2  24153  xrsmulgzz  24192  ressmulgnn  24197  ressmulgnn0  24198  xrge0addass  24203  xrge0addgt0  24206  xrge0adddir  24207  xrge0npcan  24208  fsumrp0cl  24209  xrge0tsmsd  24215  dvrdir  24218  rdivmuldivd  24219  dvrcan5  24221  elrhmunit  24250  rhmunitinv  24252  cnre2csqima  24301  tpr2rico  24302  cnvordtrestixx  24303  xrge0iifcnv  24311  xrge0iifhom  24315  xrge0mulc1cn  24319  rge0scvg  24327  lmxrge0  24329  cnzh  24346  rezh  24347  qqhval2  24358  qqhvq  24363  qqhnm  24366  qqhcn  24367  qqhucn  24368  indsum  24412  indf1ofs  24415  esumel  24434  esumle  24441  esummono  24442  gsumesum  24443  esumlub  24444  esumlef  24446  esumcst  24447  esumfzf  24451  esumfsup  24452  esumfsupre  24453  esumpinfval  24455  esumpfinvallem  24456  esumpfinval  24457  esumpfinvalf  24458  esumpinfsum  24459  esumpcvgval  24460  esumpmono  24461  esummulc1  24463  esummulc2  24464  esumdivc  24465  hasheuni  24467  esumcvg  24468  sigainb  24511  measun  24557  measunl  24562  measiun  24564  meascnbl  24565  voliune  24577  volfiniune  24578  dya2icoseg2  24620  dya2iocnrect  24623  sxbrsigalem2  24628  sibfof  24646  probun  24669  probdif  24670  probvalrnd  24674  probmeasb  24680  cndprobin  24684  bayesth  24689  ballotlemsdom  24761  ballotlemrv2  24771  ballotlemfrci  24777  lgamgulmlem2  24806  lgamcvg2  24831  subfacp1lem5  24862  erdszelem4  24872  erdszelem6  24874  erdszelem7  24875  erdszelem8  24876  erdszelem9  24877  conpcon  24914  cvxscon  24922  rescon  24925  iccllyscon  24929  rellyscon  24930  cvmsrcl  24943  cvmliftmolem2  24961  cvmlift2lem12  24993  cvmlift3  25007  snmlval  25010  clim2prod  25208  ntrivcvg  25217  ntrivcvgfvn0  25219  ntrivcvgtail  25220  ntrivcvgmullem  25221  ntrivcvgmul  25222  prodrblem  25247  prodmolem2a  25252  axlowdimlem16  25888  axcontlem10  25904  mblfinlem  26234  itg2addnclem3  26248  itg2addnc  26249  itg2gt0cn  26250  ftc1cnnclem  26268  ftc1anclem6  26275  islocfin  26367  neibastop1  26379  fdc  26440  prdsbnd  26493  ismtyval  26500  heiborlem3  26513  heiborlem5  26515  heiborlem10  26520  rrnequiv  26535  eldiophb  26806  4rexfrabdioph  26849  6rexfrabdioph  26850  diophren  26865  rencldnfilem  26872  pellexlem3  26885  pellfundglb  26939  rmxypairf1o  26965  rmxycomplete  26971  rmxyneg  26974  rmxyadd  26975  rmxy1  26976  rmxy0  26977  monotuz  26995  jm2.22  27057  aomclem2  27121  isnumbasgrp  27240  dfacbasgrp  27241  hbtlem2  27296  hbt  27302  elmnc  27309  symggen  27379  symgtrinv  27381  psgnunilem5  27385  psgnunilem2  27386  psgnuni  27390  issdrg  27473  cntzsdrg  27478  mon1psubm  27493  stoweidlem26  27742  stoweidlem51  27767  lswrdcshw  28229  suctrALT3  28973  chordthmALT  28982  iunconlem2  28984  bnj1213  29107  bnj1417  29347  osumcllem7N  30696  pexmidlem4N  30707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator