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

Theorem sseli 3439
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1  |-  A  C_  B
Assertion
Ref Expression
sseli  |-  ( C  e.  A  ->  C  e.  B )

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2  |-  A  C_  B
2 ssel 3437 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2ax-mp 5 1  |-  ( C  e.  A  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429
This theorem is referenced by:  sselii  3440  sseldi  3441  elun1  3612  elun2  3613  elopabran  4752  copsex2ga  4964  issref  5231  2elresin  5708  nfvres  5917  fvco4i  5965  mptrcl  5977  fvmptss  5980  fvmptex  5982  fvmptnf  5989  elfvmptrab1  5992  fvopab4ndm  5994  fvimacnvi  6018  elpreima  6024  iinpreima  6032  ofrfval  6565  ofval  6566  off  6572  nnon  6724  finds  6745  finds2  6747  offres  6814  eqopi  6853  op1steq  6861  dfoprab4  6876  bropopvvv  6900  bropfvvvv  6902  curry1val  6915  curry2val  6919  reldmtpos  7006  wfrlem4  7064  wfrlem10  7070  smores3  7097  smores2  7098  frsuc  7179  nnfi  7790  unifpw  7902  f1opwfi  7903  fival  7951  fi0  7959  dffi2  7962  elfiun  7969  cantnfp1lem1  8208  cantnfp1lem3  8210  epfrs  8240  r1fin  8269  r1tr  8272  r1ordg  8274  r1ord3g  8275  r1val1  8282  tz9.12lem3  8285  tcrank  8380  cplem1  8385  hta  8393  tskwe  8409  cardprclem  8438  r0weon  8468  fodomfi2  8516  alephfplem3  8562  dfac12r  8601  ackbij1lem6  8680  ackbij1lem9  8683  ackbij1lem10  8684  ackbij1lem11  8685  ackbij1lem16  8690  ackbij1lem18  8692  ackbij2  8698  fin23lem24  8777  fin23lem26  8780  fin23lem28  8795  fin23lem30  8797  fin23lem31  8798  isfin1-3  8841  fin1a2lem6  8860  hsmexlem4  8884  hsmexlem5  8885  hsmexlem6  8886  axdc2lem  8903  axdc3lem2  8906  axcclem  8912  ac6num  8934  brdom5  8982  brdom4  8983  canthp1lem2  9103  r1tskina  9232  gruina  9268  grur1a  9269  pinn  9328  0nnq  9374  elpqn  9375  recn  9654  rexr  9711  dedekindle  9823  ltord1  10167  leord1  10168  eqord1  10169  nnre  10643  nncn  10644  nnind  10654  nnnn0  10904  nn0re  10906  nn0cn  10907  nnz  10987  nn0z  10988  nnq  11305  qcn  11306  rpre  11336  difreicc  11792  iccshftri  11795  iccshftli  11797  iccdili  11799  icccntri  11801  fzval2  11815  fzelp1  11876  4fvwrd4  11939  elfzo1  11995  ico01fl0  12084  expcllem  12314  expcl2lem  12315  m1expcl2  12325  bcm1k  12531  bcpasc  12537  hashbclem  12647  swrd0fv0  12832  swrd0fvlsw  12835  sqrlem5  13358  cau3lem  13465  caubnd  13469  climconst2  13660  rlimres  13670  lo1res  13671  lo1resb  13676  rlimresb  13677  o1resb  13678  o1of2  13724  o1rlimmul  13730  caurcvg  13790  caurcvgOLD  13791  caucvg  13793  ackbijnn  13934  binomlem  13935  incexclem  13942  divcnvshft  13961  zprod  14039  fprodge1  14097  risefaccllem  14114  fallfaccllem  14115  bpolydiflem  14155  bpoly4  14160  divalglem8  14428  sadadd  14489  smueqlem  14512  smumul  14515  isprm3  14681  phimullem  14775  prmdiveq  14782  unbenlem  14900  prmreclem2  14909  prmrec  14914  vdwnnlem1  14993  vdwnnlem3  14995  ramtcl2  15014  ramtcl2OLD  15015  prmgaplem4  15072  cshwshashlem1  15114  isstruct2  15178  structcnvcnv  15180  fvsetsid  15196  strlemor1  15265  imasdsval2  15465  imasdsval2OLD  15477  xpsfrnel2  15519  mreunirn  15555  mrcfval  15562  mrisval  15584  isacs2  15607  acsfn  15613  homarcl  15971  arwval  15986  coafval  16007  coapm  16014  isdrs2  16232  isacs3lem  16460  psssdm2  16509  tsrss  16517  submnd0  16614  nmzsubg  16906  nmznsg  16909  resscntz  17033  cntzmhm  17040  symgtrinv  17161  pmtrdifellem4  17168  psgnpmtr  17199  efginvrel2  17425  efginvrel1  17426  efgsp1  17435  efgsres  17436  efgsfo  17437  frgpinv  17462  frgpupf  17471  frgpup1  17473  subcmn  17525  torsubg  17540  dprd2dlem1  17722  dpjidcl  17739  ablfaclem3  17768  subrgpropd  18090  lssacs  18238  sralmod  18458  psrbaglefi  18644  mplsubglem  18706  ressmpladd  18729  ressmplmul  18730  ressmplvsca  18731  mplmonmul  18736  mplind  18773  ply1bascl  18844  cnsubdrglem  19067  rege0subm  19072  rge0srg  19086  zringunit  19110  znrrg  19184  psgnghm  19196  zrhpsgnevpm  19207  evpmodpmf1o  19212  pmtrodpm  19213  frlmsslsp  19402  islinds4  19441  lmimlbs  19442  lbslcic  19447  mdetralt  19681  mdetunilem7  19691  chfacfpmmulgsum2  19937  basdif0  20016  tgval2  20019  mreclatdemoBAD  20160  ordtbas  20256  ordtrest  20266  ordtrestixx  20286  fincmp  20456  cmpfi  20471  bwth  20473  iuncon  20491  1stcrest  20516  hauslly  20555  kgentop  20605  ptbasin  20640  ptcnplem  20684  txkgen  20715  infil  20926  filunirn  20945  uzrest  20960  elflim  21034  hauspwpwf1  21050  flffval  21052  fclsval  21071  isfcls  21072  fcfval  21096  alexsubALTlem3  21112  alexsubALTlem4  21113  ustn0  21283  fmucndlem  21354  xmetunirn  21400  blbas  21493  blres  21494  mopnval  21501  setsmstopn  21541  tmsval  21544  tngtopn  21706  qtopbaslem  21827  xrtgioo  21872  reperflem  21884  icccmplem1  21888  reconnlem2  21893  xrge0tsms  21900  icopnfhmeo  22019  icccvx  22026  bndth  22034  reparphti  22076  pcofval  22089  pcoval1  22092  pcoval2  22095  pcoass  22103  pcorevlem  22105  pcorev2  22107  pi1xfrcnv  22136  nmhmcn  22182  csscld  22268  cfilfval  22282  caufval  22293  cfilres  22314  bcthlem1  22340  ivthlem1  22450  ivthlem3  22452  ovolicc2lem3  22520  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  ioombl1lem4  22562  vitalilem1  22614  mbflimsup  22671  mbflimsupOLD  22672  i1fima2  22685  i1fd  22687  i1f0  22693  i1f1  22696  itg1addlem4  22705  itg1addlem5  22706  itg2cnlem2  22768  iblmbf  22773  ellimc2  22880  limcres  22889  limcun  22898  dvbsss  22905  perfdvf  22906  dvres2lem  22913  dvaddbr  22940  rolle  22990  cmvth  22991  dvlip  22993  dvlipcn  22994  dvle  23007  lhop1lem  23013  dvfsumle  23021  dvfsumge  23022  dvfsumabs  23023  dvfsumlem2  23027  ftc2  23044  itgparts  23047  itgsubstlem  23048  itgsubst  23049  deg1mul3  23112  coeval  23225  coeeu  23227  dgrval  23230  coef3  23234  coemulc  23257  dgrsub  23274  coecj  23280  dvply2  23287  dvnply  23289  quotval  23293  fta1  23309  plyexmo  23314  aacjcl  23331  taylfval  23362  dvtaylp  23373  abelth  23444  pilem2  23455  pilem2OLD  23456  pilem3  23457  pilem3OLD  23458  sinord  23531  recosf1o  23532  resinf1o  23533  tanord1  23534  eff1olem  23545  dvloglem  23641  dvlog  23644  dvlog2lem  23645  advlogexp  23648  logtayl  23653  logtayl2  23655  dvcncxp1  23731  dvcnsqrt  23732  cxpcn3lem  23735  cxpcn3  23736  sqrtcn  23738  loglesqrt  23746  1cubr  23816  acosrecl  23877  rlimcnp2  23940  xrlimcnp  23942  efrlim  23943  jensen  23962  lgamgulmlem2  24003  lgamucov2  24012  basellem4  24058  ppiprm  24126  chtprm  24128  prmorcht  24153  dvdsflip  24159  musum  24168  chpchtsum  24195  dchrinvcl  24229  dchrghm  24232  dchrinv  24237  dchrsum2  24244  dchrsum  24245  rplogsumlem2  24371  rpvmasumlem  24373  dchrisum0re  24399  dchrisum0lem2a  24403  dirith2  24414  pnt  24500  tglng  24639  axlowdimlem6  25025  axlowdimlem16  25035  axlowdimlem17  25036  axlowdim  25039  axeuclidlem  25040  axcontlem2  25043  axcontlem7  25048  axcontlem8  25049  clwwlknprop  25548  clwwisshclww  25583  2wlkonot3v  25651  2spthonot3v  25652  issubgoi  26086  opidonOLD  26098  flddivrng  26191  rngosn3  26202  vcoprnelem  26245  nvvcop  26261  nvex  26278  phnv  26503  sheli  26915  cheli  26933  choc1  27028  shintcli  27030  chintcli  27032  shsleji  27071  pjini  27400  mayete3i  27429  dmadjop  27589  nlelshi  27761  cnlnadjeui  27778  cnlnssadj  27781  bdopadj  27783  pjimai  27877  stcl  27917  atelch  28045  disjin  28244  disjin2  28245  fcnvgreu  28323  partfun  28326  f1od2  28357  fcobijfs  28359  xrge0infss  28388  xrge0infssOLD  28389  iundisj2fi  28421  nnindf  28430  eliccioo  28448  xrge0mulgnn0  28499  xrge0nre  28501  xrge0omnd  28522  gsummptres  28595  prsdm  28768  prsrn  28769  ordtrestNEW  28775  xrge0iifcnv  28787  xrge0iifcv  28788  xrge0iifiso  28789  xrge0iifhom  28791  qqhcn  28843  esumval  28915  gsumesum  28928  esumlub  28929  esumcst  28932  esumfsup  28939  esumcvgre  28960  issgon  28993  elrnsiga  28996  imambfm  29132  br2base  29139  sxbrsigalem0  29141  dya2iocucvr  29154  sxbrsigalem2  29156  sxbrsigalem5  29158  sxbrsiga  29160  omssubadd  29176  omssubaddOLD  29180  sitmcl  29232  oddpwdc  29235  eulerpartlemelr  29238  eulerpartgbij  29253  eulerpartlemgvv  29257  eulerpartlemgh  29259  eulerpartlemgs2  29261  eulerpartlemn  29262  sseqf  29273  ballotlem2  29369  ballotlemfp1  29372  ballotlemfc0  29373  ballotlemfcc  29374  ballotlemfmpn  29375  ballotlemsup  29385  ballotlemfrceq  29409  ballotlemsupOLD  29423  ballotlemfrceqOLD  29447  signswch  29498  bnj1533  29711  bnj1137  29852  bnj1286  29876  bnj1408  29893  bnj1417  29898  subfacp1lem5  29955  cvmsi  30036  mpst123  30226  mpstrcl  30227  msrrcl  30229  elmsta  30234  msubvrs  30246  elmpps  30259  elmthm  30262  bcprod  30422  dfon2lem4  30480  frrlem4  30565  pprodss4v  30699  ivthALT  31039  neibastop2lem  31064  nnssi2  31163  nnssi3  31164  bj-sngltagi  31620  bj-elid  31684  bj-elid2  31685  bj-cmnssmndel  31736  bj-ablssgrpel  31738  bj-ablsscmnel  31740  bj-vecssmodel  31743  bj-rrvecssvecel  31750  bj-rrvecsscmnel  31752  taupilemrplb  31765  icorempt2  31798  elxp8  31818  sin2h  31979  cos2h  31980  tan2h  31981  poimirlem14  31998  poimirlem26  32010  poimirlem27  32011  poimirlem31  32015  poimirlem32  32016  mblfinlem1  32021  cnambfre  32033  dvtan  32036  itg2addnc  32040  itg2gt0cn  32041  ftc1cnnc  32060  ftc2nc  32070  dvasin  32072  dvacos  32073  cover2  32084  sstotbnd2  32150  heibor1lem  32185  heiborlem10  32196  exidcl  32218  toycom  32583  osumcllem7N  33571  pexmidlem4N  33582  diaintclN  34670  dibintclN  34779  mapd1o  35260  hdmapevec  35450  elrfi  35580  elrfirn  35581  elrfirn2  35582  mrefg3  35594  diophin  35659  diophun  35660  eq0rabdioph  35663  eqrabdioph  35664  pellex  35723  rmxycomplete  35809  jm2.23  35895  aomclem2  35957  fglmod  35975  lsmfgcl  35976  lmhmfgima  35986  lmhmfgsplit  35988  isnumbasabl  36009  dgrsub2  36038  itgocn  36074  acsfn1p  36109  areaquad  36145  elmapintrab  36226  corcltrcl  36375  radcnvrat  36706  uzmptshftfval  36738  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  onfrALTlem2  36955  onfrALTlem2VD  37325  uzwo4  37429  disjinfi  37505  eliccxr  37649  eliccelioc  37659  elicores  37672  fsumiunss  37691  limcdm0  37735  sumnnodd  37747  cncfshift  37788  cncfperiod  37793  icccncfext  37802  dvnprodlem1  37858  dvnprodlem2  37859  itgsin0pilem1  37863  itgsinexplem1  37867  itgsinexp  37868  ditgeqiooicc  37874  itgsubsticclem  37889  itgioocnicc  37891  itgsbtaddcnst  37896  stoweidlem34  37932  stoweidlem41  37939  stoweidlem51  37949  wallispilem2  37965  stirlinglem11  37983  dirkercncflem2  38003  fourierdlem5  38011  fourierdlem9  38015  fourierdlem17  38023  fourierdlem18  38024  fourierdlem20  38026  fourierdlem39  38046  fourierdlem48  38055  fourierdlem49  38056  fourierdlem62  38069  fourierdlem66  38073  fourierdlem68  38075  fourierdlem72  38079  fourierdlem73  38080  fourierdlem81  38088  fourierdlem83  38090  fourierdlem85  38092  fourierdlem87  38094  fourierdlem88  38095  fourierdlem92  38099  fourierdlem95  38102  fourierdlem103  38110  fourierdlem104  38111  fourierdlem112  38119  sqwvfoura  38129  sqwvfourb  38130  fouriersw  38132  etransclem24  38160  etransclem35  38171  etransclem37  38173  salexct  38230  salgencntex  38239  gsumge0cl  38250  sge0tsms  38259  sge0resplit  38285  sge0split  38288  caratheodorylem1  38384  volicorescl  38412  hoidmv1lelem3  38452  opnvonmbllem2  38492  bgoldbtbndlem2  38938  bgoldbtbndlem3  38939  bgoldbtbnd  38941  pfxfv0  38980  pfxfvlsw  38983  nn0xnn0  39119  1wlk1walk  39696  pthdivtx  39761  pthdadjvtx  39762  fldhmsubc  40358  fldhmsubcALTV  40377
  Copyright terms: Public domain W3C validator