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

Theorem sseldi 3180
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 3178 . 2  |-  ( C  e.  A  ->  C  e.  B )
41, 3syl 15 1  |-  ( ph  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686    C_ wss 3154
This theorem is referenced by:  onfr  4433  sofld  5123  fvrn0  5552  elmpt2cl  6063  ofrval  6090  tpostpos  6256  opiota  6292  riotacl  6321  riotasbc  6322  smores  6371  tz7.44-2  6422  omopthlem2  6656  f1opwfi  7161  supub  7212  suplub  7213  ordtypelem3  7237  ordtypelem4  7238  ordtypelem6  7240  ordtypelem7  7241  wemapso2lem  7267  wemapso2  7269  unxpwdom2  7304  cantnfres  7381  wemapwe  7402  oef1o  7403  cnfcomlem  7404  r1pwss  7458  r1elwf  7470  rankr1ai  7472  r0weon  7642  infxpenlem  7643  acnlem  7677  acndom2  7683  infpwfien  7691  alephfp  7737  ackbij1lem18  7865  ackbij1b  7867  cflim2  7891  fin23lem26  7953  fin23lem30  7970  isf32lem5  7985  isf32lem7  7987  isf32lem8  7988  isf32lem9  7989  isfin1-3  8014  fin1a2lem9  8036  fin1a2lem11  8038  hsmexlem5  8058  zorn2lem3  8127  zorn2lem4  8128  zorn2lem5  8129  ttukeylem6  8143  ttukeylem7  8144  iundom2g  8164  fpwwe2lem12  8265  pwfseqlem3  8284  gch2  8303  wunom  8344  rexrd  8883  nnred  9763  nncnd  9764  un0addcl  9999  un0mulcl  10000  nnnn0d  10020  nn0red  10021  suprzcl  10093  nn0zd  10117  zred  10119  zsupss  10309  rpnnen1lem1  10344  rpnnen1lem2  10345  rpred  10392  fzfi  11036  seqf1olem1  11087  expcl2lem  11117  m1expcl  11128  hashxrcl  11353  seqcoll2  11404  wrdeqcats1  11476  wrdind  11479  limsupgre  11957  rlimpm  11976  rlimclim  12022  isercolllem1  12140  isercolllem2  12141  isercoll  12143  iseraltlem2  12157  iseraltlem3  12158  fsumcvg3  12204  ackbijnn  12288  bitsval  12617  bitsfzolem  12627  bitsinv1  12635  smuval2  12675  gcdcllem3  12694  eulerthlem2  12852  prmdivdiv  12857  prmreclem1  12965  prmreclem2  12966  prmreclem3  12967  1arith  12976  4sqlem13  13006  4sqlem14  13007  4sqlem17  13010  vdwlem5  13034  vdwlem8  13037  vdwlem12  13041  vdwnnlem3  13046  ramtlecl  13049  ramcl2lem  13058  ramcl2  13065  ramxrcl  13066  submrc  13532  mreexexlem2d  13549  catlid  13587  catrid  13588  sscpwex  13694  subcrcl  13695  sscres  13702  wunfunc  13775  funcres2c  13777  cofull  13810  cofth  13811  coffth  13812  rescfth  13813  homarel  13870  arwrcl  13878  idaf  13897  homdmcoa  13901  coaval  13902  coapm  13905  catciso  13941  catcoppccl  13942  catcfuccl  13943  catcxpccl  13983  acsfiindd  14282  psssdm2  14326  submrcl  14426  gsumval2  14462  issubg  14623  isnsg  14648  nmzsubg  14660  conjnmz  14718  conjnmzb  14719  cntzsubm  14813  cntzsubg  14814  odlem2  14856  gexlem2  14895  sylow1lem2  14912  sylow1lem4  14914  sylow2a  14932  efglem  15027  efgtf  15033  efgtlen  15037  efgsres  15049  efgsfo  15050  efgredlemg  15053  efgredleme  15054  efgredlemd  15055  efgredlemc  15056  efgredlem  15058  efgred  15059  efgcpbllemb  15066  frgpuplem  15083  frgpnabllem2  15164  cyggex2  15185  dprdfsub  15258  dprdf11  15260  dprd2da  15279  ablfac2  15326  isdrng2  15524  issubrg  15547  cntzsubr  15579  abvrcl  15588  lsppratlem1  15902  lsppratlem2  15903  lbsextlem3  15915  sralmod  15941  rrgeq0  16033  psrbagconf1o  16122  psrass1lem  16125  psrdi  16153  psrdir  16154  psrass23  16156  resspsrmul  16163  mplelf  16180  mplsubrglem  16185  mpladd  16188  mplmul  16189  mplvsca  16193  mplmonmul  16210  mplcoe2  16213  mplind  16245  psropprmul  16318  zlpirlem2  16444  zlpirlem3  16445  znf1o  16507  cygznlem2a  16523  ocvlss  16574  lsmcss  16594  isobs  16622  restbas  16891  ordtbas2  16923  ordtopn1  16926  ordtopn2  16927  ordtrest  16934  iocpnfordt  16947  icomnfordt  16948  lmrcl  16963  subbascn  16986  lmss  17028  hauscmplem  17135  cnconn  17150  clscon  17158  concompclo  17163  subislly  17209  cldllycmp  17223  kgeni  17234  llycmpkgen2  17247  1stckgenlem  17250  ptbasfi  17278  xkoopn  17286  txcls  17301  dfac14lem  17313  txcnp  17316  ptcnplem  17317  upxp  17319  txtube  17336  txcmplem1  17337  txcmplem2  17338  txkgen  17348  xkopt  17351  xkococnlem  17355  txcon  17385  basqtop  17404  tgqtop  17405  kqnrmlem1  17436  kqnrmlem2  17437  nrmhmph  17487  ptcmpfi  17506  elmptrab  17524  uzrest  17594  fclsfnflim  17724  flimfnfcls  17725  cnpfcf  17738  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem2  17749  ptcmplem5  17752  tsmsres  17828  prdsxmetlem  17934  imasdsf1olem  17939  isxms2  17996  prdsbl  18039  met2ndci  18070  nmdvr  18183  nrginvrcnlem  18203  nrginvrcn  18204  tgqioo  18308  zdis  18324  reperflem  18325  reconnlem2  18334  reconn  18335  xrge0gsumle  18340  xrge0tsms  18341  xmetdcn  18345  metdcn  18347  metdscn2  18363  cncfmpt2ss  18421  icchmeo  18441  iccpnfcnv  18444  xrhmeo  18446  icccvx  18450  cnheibor  18455  bndth  18458  evth  18459  lebnum  18464  isphtpc  18494  reparphti  18497  pcoass  18524  nmoleub2lem  18597  nmoleub2lem3  18598  nmoleub2lem2  18599  nmoleub3  18602  nmhmcn  18603  cfili  18696  cfilfcls  18702  caussi  18725  equivcau  18728  minveclem4b  18797  minveclem4  18798  evthicc2  18822  ovolfcl  18828  ovolfioo  18829  ovolficc  18830  ovolficcss  18831  ovolfsval  18832  ovolmge0  18838  ovollb2lem  18849  ovolunlem1a  18857  ovoliunlem1  18863  ovolicc1  18877  ovolicc2lem4  18881  ovolicc2lem5  18882  ioombl1lem2  18918  ioombl1lem4  18920  ovolfs2  18928  ioorcl  18934  uniiccdif  18935  uniioovol  18936  uniiccvol  18937  uniioombllem2a  18939  uniioombllem2  18940  uniioombllem3a  18941  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombllem6  18945  dyadmbl  18957  volsup2  18962  volivth  18964  vitalilem1  18965  vitalilem2  18966  vitalilem4  18968  mbfimaopnlem  19012  cncombf  19015  cnmbf  19016  mbflimsup  19023  mbfi1fseqlem3  19074  mbfi1fseqlem4  19075  mbfi1fseqlem5  19076  itg2const2  19098  itg2lea  19101  itg2eqa  19102  itg2split  19106  itg2i1fseq  19112  itg2gt0  19117  limcco  19245  dvcl  19251  perfdvf  19255  dvreslem  19261  dvres2lem  19262  dvidlem  19267  dvcnp2  19271  dvmulbr  19290  dvrec  19306  dvferm1lem  19333  dvferm2lem  19335  dvferm  19337  rolle  19339  dvlipcn  19343  dvlip2  19344  c1liplem1  19345  c1lip2  19347  dvgt0lem1  19351  dvivthlem1  19357  dvivth  19359  lhop1lem  19362  lhop1  19363  lhop2  19364  lhop  19365  dvfsumlem1  19375  dvfsumlem2  19376  dvfsumlem3  19377  dvfsumlem4  19378  dvfsumrlimge0  19379  dvfsumrlim  19380  dvfsumrlim2  19381  dvfsum2  19383  ftc1lem5  19389  ftc1lem6  19390  itgsubstlem  19397  itgsubst  19398  mdegleb  19452  mdegaddle  19462  mdegvsca  19464  mdegmullem  19466  ig1peu  19559  plybss  19578  plyaddcl  19604  plymulcl  19605  plysubcl  19606  coeidlem  19621  coesub  19640  dgrmulc  19654  dgrcolem1  19656  dgrcolem2  19657  dgrco  19658  quotlem  19682  quotcl2  19684  quotdgr  19685  plyrem  19687  facth  19688  quotcan  19691  vieta1lem1  19692  vieta1  19694  elqaalem3  19703  aalioulem2  19715  aalioulem3  19716  taylfvallem1  19738  tayl0  19743  dvntaylp  19752  taylthlem1  19754  taylthlem2  19755  radcnvlt1  19796  radcnvle  19798  pserulm  19800  psercnlem2  19802  psercnlem1  19803  psercn  19804  pserdvlem1  19805  pserdvlem2  19806  abelthlem3  19811  abelthlem5  19813  abelthlem6  19814  abelth  19819  efcvx  19827  tanord  19902  tanregt0  19903  efif1olem4  19909  logtayl  20009  logccv  20012  cxpcn3  20090  ssscongptld  20124  chordthmlem  20131  chordthmlem4  20134  chordthmlem5  20135  chordthm  20136  asinrecl  20200  atantan  20221  dvatan  20233  leibpi  20240  rlimcnp  20262  efrlim  20266  cvxcl  20281  scvxcvx  20282  jensenlem1  20283  jensenlem2  20284  jensen  20285  amgmlem  20286  harmonicbnd3  20303  wilthlem1  20308  ftalem3  20314  ftalem5  20316  ftalem7  20318  basellem3  20322  basellem4  20323  basellem5  20324  ppisval  20343  chtf  20348  efchtcl  20351  chtge0  20352  sgmval2  20383  ppinprm  20392  chtprm  20393  chtnprm  20394  chtwordi  20396  chtdif  20398  efchtdvds  20399  sqff1o  20422  fsumdvdsdiaglem  20425  fsumdvdsdiag  20426  fsumdvdscom  20427  musum  20433  muinv  20435  dvdsmulf1o  20436  sgmmul  20442  chtlepsi  20447  chtleppi  20451  pclogsum  20456  chpval2  20459  chpchtsum  20460  chpub  20461  perfectlem2  20471  dchrelbasd  20480  dchrrcl  20481  dchrzrh1  20485  dchrzrhmul  20487  dchrinvcl  20494  dchrfi  20496  dchrghm  20497  dchr1  20498  dchrabs  20501  dchrinv  20502  dchrptlem2  20506  dchrsum2  20509  sumdchr2  20511  sum2dchr  20515  lgscl  20551  lgsquadlem1  20595  lgsquadlem2  20596  2sqlem6  20610  2sqlem8  20613  2sqlem9  20614  chebbnd1lem1  20620  chtppilimlem1  20624  rplogsumlem2  20636  dchrisum0flblem1  20659  rpvmasum2  20663  dchrisum0re  20664  dchrisum0lema  20665  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2a  20668  dchrisum0lem2  20669  dchrisum0lem3  20670  dchrisum0  20671  rplogsum  20678  dirith2  20679  mudivsum  20681  mulogsum  20683  mulog2sumlem2  20686  vmalogdivsum2  20689  logsqvma  20693  logsqvma2  20694  selberglem3  20698  selberg  20699  chpdifbndlem1  20704  selberg34r  20722  pntsval2  20727  pntrlog2bndlem1  20728  pntpbnd1a  20736  pntpbnd1  20737  pntpbnd2  20738  pntibndlem2a  20741  pntibndlem2  20742  pntibndlem3  20743  pntlemd  20745  padicabv  20781  issubgo  20972  nvvop  21167  nmcnc  21271  ubthlem1  21451  minvecolem2  21456  minvecolem3  21457  minvecolem5  21462  minvecolem6  21463  minvecolem7  21464  hlimcaui  21818  pjocini  22279  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemimin  23066  ballotlemsdom  23072  ballotlemrv2  23082  ballotlemfrci  23088  eliccelico  23272  elicoelioo  23273  ssnnssfz  23279  cnre2csqima  23297  tpr2rico  23298  cnvordtrestixx  23299  xrsmulgzz  23309  ressmulgnn  23310  ressmulgnn0  23311  xrge0iifcnv  23317  xrge0iifhom  23321  xrge0mulc1cn  23325  xrge0addass  23331  xrge0addgt0  23333  xrge0adddir  23334  fsumrp0cl  23336  iundisjfi  23365  iundisj2fi  23366  rge0scvg  23375  lmxrge0  23377  xrge0tsmsd  23384  esumle  23435  esumlef  23437  esumcst  23438  esumpinfval  23443  esumpfinvallem  23444  esumpfinval  23445  esumpfinvalf  23446  esumpinfsum  23447  esumpcvgval  23448  esumpmono  23449  esummulc1  23451  esummulc2  23452  esumdivc  23453  hasheuni  23455  esumcvg  23456  sigainb  23499  measxun  23541  measiun  23547  meascnbl  23548  indsum  23608  indf1ofs  23611  probun  23624  probdif  23625  probvalrnd  23629  cndprobin  23639  bayesth  23644  dstrvprob  23674  coinfliplem  23681  subfacp1lem5  23717  erdszelem4  23727  erdszelem6  23729  erdszelem7  23730  erdszelem8  23731  erdszelem9  23732  conpcon  23768  cvxscon  23776  rescon  23779  iccllyscon  23783  rellyscon  23784  cvmsrcl  23797  cvmliftmolem2  23815  cvmlift2lem12  23847  cvmlift3  23861  umgrass  23873  umgran0  23874  umgraex  23877  snmlval  23916  axlowdimlem16  24587  axcontlem10  24603  inposet  25289  besubbeca  25859  pfsubkl  26058  islocfin  26307  neibastop1  26319  fdc  26466  prdsbnd  26528  ismtyval  26535  heiborlem3  26548  heiborlem5  26550  heiborlem10  26555  rrnequiv  26570  eldiophb  26847  4rexfrabdioph  26890  6rexfrabdioph  26891  diophren  26907  rencldnfilem  26914  pellexlem3  26927  pellfundglb  26981  rmxypairf1o  27007  rmxycomplete  27013  rmxyneg  27016  rmxyadd  27017  rmxy1  27018  rmxy0  27019  monotuz  27037  jm2.22  27099  aomclem2  27163  isnumbasgrp  27283  dfacbasgrp  27284  hbtlem2  27339  hbt  27345  elmnc  27352  pmtrfinv  27413  symggen  27422  symgtrinv  27424  psgnunilem5  27428  psgnunilem2  27429  psgnuni  27433  issdrg  27516  cntzsdrg  27521  mon1psubm  27536  wallispilem4  27828  mpt2xopn0yelv  28090  mpt2xopxnop0  28092  usgrass  28121  nbgrael  28152  suctrALT3  28773  chordthmALT  28783  bnj1213  28904  bnj1417  29144  osumcllem7N  30224  pexmidlem4N  30235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator