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

Theorem sseldi 3178
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 3176 . 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 1684    C_ wss 3152
This theorem is referenced by:  onfr  4431  sofld  5121  fvrn0  5550  elmpt2cl  6061  ofrval  6088  tpostpos  6254  opiota  6290  riotacl  6319  riotasbc  6320  smores  6369  tz7.44-2  6420  omopthlem2  6654  f1opwfi  7159  supub  7210  suplub  7211  ordtypelem3  7235  ordtypelem4  7236  ordtypelem6  7238  ordtypelem7  7239  wemapso2lem  7265  wemapso2  7267  unxpwdom2  7302  cantnfres  7379  wemapwe  7400  oef1o  7401  cnfcomlem  7402  r1pwss  7456  r1elwf  7468  rankr1ai  7470  r0weon  7640  infxpenlem  7641  acnlem  7675  acndom2  7681  infpwfien  7689  alephfp  7735  ackbij1lem18  7863  ackbij1b  7865  cflim2  7889  fin23lem26  7951  fin23lem30  7968  isf32lem5  7983  isf32lem7  7985  isf32lem8  7986  isf32lem9  7987  isfin1-3  8012  fin1a2lem9  8034  fin1a2lem11  8036  hsmexlem5  8056  zorn2lem3  8125  zorn2lem4  8126  zorn2lem5  8127  ttukeylem6  8141  ttukeylem7  8142  iundom2g  8162  fpwwe2lem12  8263  pwfseqlem3  8282  gch2  8301  wunom  8342  rexrd  8881  nnred  9761  nncnd  9762  un0addcl  9997  un0mulcl  9998  nnnn0d  10018  nn0red  10019  suprzcl  10091  nn0zd  10115  zred  10117  zsupss  10307  rpnnen1lem1  10342  rpnnen1lem2  10343  rpred  10390  fzfi  11034  seqf1olem1  11085  expcl2lem  11115  m1expcl  11126  hashxrcl  11351  seqcoll2  11402  wrdeqcats1  11474  wrdind  11477  limsupgre  11955  rlimpm  11974  rlimclim  12020  isercolllem1  12138  isercolllem2  12139  isercoll  12141  iseraltlem2  12155  iseraltlem3  12156  fsumcvg3  12202  ackbijnn  12286  bitsval  12615  bitsfzolem  12625  bitsinv1  12633  smuval2  12673  gcdcllem3  12692  eulerthlem2  12850  prmdivdiv  12855  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  1arith  12974  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  vdwlem5  13032  vdwlem8  13035  vdwlem12  13039  vdwnnlem3  13044  ramtlecl  13047  ramcl2lem  13056  ramcl2  13063  ramxrcl  13064  submrc  13530  mreexexlem2d  13547  catlid  13585  catrid  13586  sscpwex  13692  subcrcl  13693  sscres  13700  wunfunc  13773  funcres2c  13775  cofull  13808  cofth  13809  coffth  13810  rescfth  13811  homarel  13868  arwrcl  13876  idaf  13895  homdmcoa  13899  coaval  13900  coapm  13903  catciso  13939  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  acsfiindd  14280  psssdm2  14324  submrcl  14424  gsumval2  14460  issubg  14621  isnsg  14646  nmzsubg  14658  conjnmz  14716  conjnmzb  14717  cntzsubm  14811  cntzsubg  14812  odlem2  14854  gexlem2  14893  sylow1lem2  14910  sylow1lem4  14912  sylow2a  14930  efglem  15025  efgtf  15031  efgtlen  15035  efgsres  15047  efgsfo  15048  efgredlemg  15051  efgredleme  15052  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  efgred  15057  efgcpbllemb  15064  frgpuplem  15081  frgpnabllem2  15162  cyggex2  15183  dprdfsub  15256  dprdf11  15258  dprd2da  15277  ablfac2  15324  isdrng2  15522  issubrg  15545  cntzsubr  15577  abvrcl  15586  lsppratlem1  15900  lsppratlem2  15901  lbsextlem3  15913  sralmod  15939  rrgeq0  16031  psrbagconf1o  16120  psrass1lem  16123  psrdi  16151  psrdir  16152  psrass23  16154  resspsrmul  16161  mplelf  16178  mplsubrglem  16183  mpladd  16186  mplmul  16187  mplvsca  16191  mplmonmul  16208  mplcoe2  16211  mplind  16243  psropprmul  16316  zlpirlem2  16442  zlpirlem3  16443  znf1o  16505  cygznlem2a  16521  ocvlss  16572  lsmcss  16592  isobs  16620  restbas  16889  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  ordtrest  16932  iocpnfordt  16945  icomnfordt  16946  lmrcl  16961  subbascn  16984  lmss  17026  hauscmplem  17133  cnconn  17148  clscon  17156  concompclo  17161  subislly  17207  cldllycmp  17221  kgeni  17232  llycmpkgen2  17245  1stckgenlem  17248  ptbasfi  17276  xkoopn  17284  txcls  17299  dfac14lem  17311  txcnp  17314  ptcnplem  17315  upxp  17317  txtube  17334  txcmplem1  17335  txcmplem2  17336  txkgen  17346  xkopt  17349  xkococnlem  17353  txcon  17383  basqtop  17402  tgqtop  17403  kqnrmlem1  17434  kqnrmlem2  17435  nrmhmph  17485  ptcmpfi  17504  elmptrab  17522  uzrest  17592  fclsfnflim  17722  flimfnfcls  17723  cnpfcf  17736  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  ptcmplem5  17750  tsmsres  17826  prdsxmetlem  17932  imasdsf1olem  17937  isxms2  17994  prdsbl  18037  met2ndci  18068  nmdvr  18181  nrginvrcnlem  18201  nrginvrcn  18202  tgqioo  18306  zdis  18322  reperflem  18323  reconnlem2  18332  reconn  18333  xrge0gsumle  18338  xrge0tsms  18339  xmetdcn  18343  metdcn  18345  metdscn2  18361  cncfmpt2ss  18419  icchmeo  18439  iccpnfcnv  18442  xrhmeo  18444  icccvx  18448  cnheibor  18453  bndth  18456  evth  18457  lebnum  18462  isphtpc  18492  reparphti  18495  pcoass  18522  nmoleub2lem  18595  nmoleub2lem3  18596  nmoleub2lem2  18597  nmoleub3  18600  nmhmcn  18601  cfili  18694  cfilfcls  18700  caussi  18723  equivcau  18726  minveclem4b  18795  minveclem4  18796  evthicc2  18820  ovolfcl  18826  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsval  18830  ovolmge0  18836  ovollb2lem  18847  ovolunlem1a  18855  ovoliunlem1  18861  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1lem2  18916  ioombl1lem4  18918  ovolfs2  18926  ioorcl  18932  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombllem6  18943  dyadmbl  18955  volsup2  18960  volivth  18962  vitalilem1  18963  vitalilem2  18964  vitalilem4  18966  mbfimaopnlem  19010  cncombf  19013  cnmbf  19014  mbflimsup  19021  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  itg2const2  19096  itg2lea  19099  itg2eqa  19100  itg2split  19104  itg2i1fseq  19110  itg2gt0  19115  limcco  19243  dvcl  19249  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvmulbr  19288  dvrec  19304  dvferm1lem  19331  dvferm2lem  19333  dvferm  19335  rolle  19337  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip2  19345  dvgt0lem1  19349  dvivthlem1  19355  dvivth  19357  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlimge0  19377  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsum2  19381  ftc1lem5  19387  ftc1lem6  19388  itgsubstlem  19395  itgsubst  19396  mdegleb  19450  mdegaddle  19460  mdegvsca  19462  mdegmullem  19464  ig1peu  19557  plybss  19576  plyaddcl  19602  plymulcl  19603  plysubcl  19604  coeidlem  19619  coesub  19638  dgrmulc  19652  dgrcolem1  19654  dgrcolem2  19655  dgrco  19656  quotlem  19680  quotcl2  19682  quotdgr  19683  plyrem  19685  facth  19686  quotcan  19689  vieta1lem1  19690  vieta1  19692  elqaalem3  19701  aalioulem2  19713  aalioulem3  19714  taylfvallem1  19736  tayl0  19741  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  radcnvlt1  19794  radcnvle  19796  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  abelthlem3  19809  abelthlem5  19811  abelthlem6  19812  abelth  19817  efcvx  19825  tanord  19900  tanregt0  19901  efif1olem4  19907  logtayl  20007  logccv  20010  cxpcn3  20088  ssscongptld  20122  chordthmlem  20129  chordthmlem4  20132  chordthmlem5  20133  chordthm  20134  asinrecl  20198  atantan  20219  dvatan  20231  leibpi  20238  rlimcnp  20260  efrlim  20264  cvxcl  20279  scvxcvx  20280  jensenlem1  20281  jensenlem2  20282  jensen  20283  amgmlem  20284  harmonicbnd3  20301  wilthlem1  20306  ftalem3  20312  ftalem5  20314  ftalem7  20316  basellem3  20320  basellem4  20321  basellem5  20322  ppisval  20341  chtf  20346  efchtcl  20349  chtge0  20350  sgmval2  20381  ppinprm  20390  chtprm  20391  chtnprm  20392  chtwordi  20394  chtdif  20396  efchtdvds  20397  sqff1o  20420  fsumdvdsdiaglem  20423  fsumdvdsdiag  20424  fsumdvdscom  20425  musum  20431  muinv  20433  dvdsmulf1o  20434  sgmmul  20440  chtlepsi  20445  chtleppi  20449  pclogsum  20454  chpval2  20457  chpchtsum  20458  chpub  20459  perfectlem2  20469  dchrelbasd  20478  dchrrcl  20479  dchrzrh1  20483  dchrzrhmul  20485  dchrinvcl  20492  dchrfi  20494  dchrghm  20495  dchr1  20496  dchrabs  20499  dchrinv  20500  dchrptlem2  20504  dchrsum2  20507  sumdchr2  20509  sum2dchr  20513  lgscl  20549  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem6  20608  2sqlem8  20611  2sqlem9  20612  chebbnd1lem1  20618  chtppilimlem1  20622  rplogsumlem2  20634  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrisum0  20669  rplogsum  20676  dirith2  20677  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  vmalogdivsum2  20687  logsqvma  20691  logsqvma2  20692  selberglem3  20696  selberg  20697  chpdifbndlem1  20702  selberg34r  20720  pntsval2  20725  pntrlog2bndlem1  20726  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2a  20739  pntibndlem2  20740  pntibndlem3  20741  pntlemd  20743  padicabv  20779  issubgo  20970  nvvop  21165  nmcnc  21269  ubthlem1  21449  minvecolem2  21454  minvecolem3  21455  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  hlimcaui  21816  pjocini  22277  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemimin  23064  ballotlemsdom  23070  ballotlemrv2  23080  ballotlemfrci  23086  eliccelico  23270  elicoelioo  23271  ssnnssfz  23277  cnre2csqima  23295  tpr2rico  23296  cnvordtrestixx  23297  xrsmulgzz  23307  ressmulgnn  23308  ressmulgnn0  23309  xrge0iifcnv  23315  xrge0iifhom  23319  xrge0mulc1cn  23323  xrge0addass  23329  xrge0addgt0  23331  xrge0adddir  23332  fsumrp0cl  23334  iundisjfi  23363  iundisj2fi  23364  rge0scvg  23373  lmxrge0  23375  xrge0tsmsd  23382  esumle  23433  esumlef  23435  esumcst  23436  esumpinfval  23441  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumpinfsum  23445  esumpcvgval  23446  esumpmono  23447  esummulc1  23449  esummulc2  23450  esumdivc  23451  hasheuni  23453  esumcvg  23454  sigainb  23497  measxun  23539  measiun  23545  meascnbl  23546  indsum  23606  indf1ofs  23609  probun  23622  probdif  23623  probvalrnd  23627  cndprobin  23637  bayesth  23642  dstrvprob  23672  coinfliplem  23679  subfacp1lem5  23715  erdszelem4  23725  erdszelem6  23727  erdszelem7  23728  erdszelem8  23729  erdszelem9  23730  conpcon  23766  cvxscon  23774  rescon  23777  iccllyscon  23781  rellyscon  23782  cvmsrcl  23795  cvmliftmolem2  23813  cvmlift2lem12  23845  cvmlift3  23859  umgrass  23871  umgran0  23872  umgraex  23875  snmlval  23914  axlowdimlem16  24585  axcontlem10  24601  inposet  25278  besubbeca  25848  pfsubkl  26047  islocfin  26296  neibastop1  26308  fdc  26455  prdsbnd  26517  ismtyval  26524  heiborlem3  26537  heiborlem5  26539  heiborlem10  26544  rrnequiv  26559  eldiophb  26836  4rexfrabdioph  26879  6rexfrabdioph  26880  diophren  26896  rencldnfilem  26903  pellexlem3  26916  pellfundglb  26970  rmxypairf1o  26996  rmxycomplete  27002  rmxyneg  27005  rmxyadd  27006  rmxy1  27007  rmxy0  27008  monotuz  27026  jm2.22  27088  aomclem2  27152  isnumbasgrp  27272  dfacbasgrp  27273  hbtlem2  27328  hbt  27334  elmnc  27341  pmtrfinv  27402  symggen  27411  symgtrinv  27413  psgnunilem5  27417  psgnunilem2  27418  psgnuni  27422  issdrg  27505  cntzsdrg  27510  mon1psubm  27525  wallispilem4  27817  mpt2xopn0yelv  28079  mpt2xopxnop0  28081  usgrass  28110  nbgrael  28141  suctrALT3  28700  chordthmALT  28710  bnj1213  28831  bnj1417  29071  osumcllem7N  30151  pexmidlem4N  30162
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