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

Theorem sseli 3500
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 3498 . 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 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sselii  3501  sseldi  3502  elun1  3671  elun2  3672  copsex2ga  5112  issref  5378  2elresin  5690  nfvres  5894  fvco4i  5943  fvmptss  5956  fvmptex  5958  fvmptnf  5965  elfvmptrab1  5968  fvopab4ndm  5970  fvimacnvi  5993  elpreima  5999  iinpreima  6009  ofrfval  6530  ofval  6531  off  6536  nnon  6684  finds  6704  finds2  6706  offres  6776  eqopi  6815  op1steq  6823  dfoprab4  6838  bropopvvv  6860  curry1val  6873  curry2val  6877  reldmtpos  6960  smores3  7021  smores2  7022  frsuc  7099  nnfi  7707  unifpw  7819  f1opwfi  7820  fival  7868  fi0  7876  dffi2  7879  elfiun  7886  cantnfp1lem1  8093  cantnfp1lem3  8095  cantnfp1lem1OLD  8119  cantnfp1lem3OLD  8121  epfrs  8158  r1fin  8187  r1tr  8190  r1ordg  8192  r1ord3g  8193  r1val1  8200  tz9.12lem3  8203  tcrank  8298  cplem1  8303  hta  8311  tskwe  8327  cardprclem  8356  r0weon  8386  fodomfi2  8437  alephfplem3  8483  dfac12r  8522  ackbij1lem6  8601  ackbij1lem9  8604  ackbij1lem10  8605  ackbij1lem11  8606  ackbij1lem16  8611  ackbij1lem18  8613  ackbij2  8619  fin23lem24  8698  fin23lem26  8701  fin23lem28  8716  fin23lem30  8718  fin23lem31  8719  isfin1-3  8762  fin1a2lem6  8781  hsmexlem4  8805  hsmexlem5  8806  hsmexlem6  8807  axdc2lem  8824  axdc3lem2  8827  axcclem  8833  ac6num  8855  brdom5  8903  brdom4  8904  canthp1lem2  9027  r1tskina  9156  gruina  9192  grur1a  9193  pinn  9252  0nnq  9298  elpqn  9299  recn  9578  rexr  9635  dedekindle  9740  ltord1  10075  leord1  10076  eqord1  10077  nnre  10539  nncn  10540  nnind  10550  nnnn0  10798  nn0re  10800  nn0cn  10801  nnz  10882  nn0z  10883  nnq  11191  qcn  11192  rpre  11222  difreicc  11648  iccshftri  11651  iccshftli  11653  iccdili  11655  icccntri  11657  fzval2  11671  fzelp1  11728  4fvwrd4  11786  elfzo1  11835  expcllem  12140  expcl2lem  12141  m1expcl2  12151  bcm1k  12355  bcpasc  12361  hashbclem  12461  swrd0fv0  12624  swrd0fvlsw  12627  seqshft  12875  sqrlem5  13037  cau3lem  13143  caubnd  13147  climconst2  13327  rlimres  13337  lo1res  13338  lo1resb  13343  rlimresb  13344  o1resb  13345  o1of2  13391  o1rlimmul  13397  caurcvg  13455  caucvg  13457  ackbijnn  13596  binomlem  13597  incexclem  13604  divalglem8  13910  sadadd  13969  smueqlem  13992  smumul  13995  isprm3  14078  phimullem  14161  prmdiveq  14168  unbenlem  14278  prmreclem2  14287  prmrec  14292  vdwnnlem1  14365  vdwnnlem3  14367  ramtcl2  14381  cshwshashlem1  14431  isstruct2  14492  structcnvcnv  14494  fvsetsid  14508  strlemor1  14575  imasdsval2  14764  xpsfrnel2  14813  mreunirn  14849  mrcfval  14856  mrisval  14878  isacs2  14901  acsfn  14907  homarcl  15206  arwval  15221  coafval  15242  coapm  15249  isdrs2  15419  isacs3lem  15646  psssdm2  15695  tsrss  15703  submnd0  15761  nmzsubg  16034  nmznsg  16037  resscntz  16161  cntzmhm  16168  symgtrinv  16290  pmtrdifellem4  16297  psgnpmtr  16328  efginvrel2  16538  efginvrel1  16539  efgsp1  16548  efgsres  16549  efgsfo  16550  frgpinv  16575  frgpupf  16584  frgpup1  16586  subcmn  16635  torsubg  16650  dprd2dlem1  16877  dpjidcl  16894  dpjidclOLD  16901  ablfaclem3  16925  subrgpropd  17243  lssacs  17393  sralmod  17613  psrbaglefi  17791  psrbaglefiOLD  17792  mplsubglem  17861  mplsubglemOLD  17863  ressmpladd  17887  ressmplmul  17888  ressmplvsca  17889  mplmonmul  17894  mplind  17935  ply1bascl  18010  cnsubdrglem  18234  rege0subm  18239  rge0srg  18252  zringunit  18284  zrngunit  18285  znrrg  18368  psgnghm  18380  zrhpsgnevpm  18391  evpmodpmf1o  18396  pmtrodpm  18397  frlmsslsp  18593  frlmsslspOLD  18594  islinds4  18634  lmimlbs  18635  lbslcic  18640  mdetralt  18874  mdetunilem7  18884  chfacfpmmulgsum2  19130  basdif0  19218  tgval2  19221  mreclatdemoBAD  19360  ordtbas  19456  ordtrest  19466  ordtrestixx  19486  fincmp  19656  cmpfi  19671  bwth  19673  iuncon  19692  1stcrest  19717  hauslly  19756  kgentop  19775  ptbasin  19810  ptcnplem  19854  txkgen  19885  infil  20096  filunirn  20115  uzrest  20130  elflim  20204  hauspwpwf1  20220  flffval  20222  fclsval  20241  isfcls  20242  fcfval  20266  alexsubALTlem3  20281  alexsubALTlem4  20282  ustn0  20455  fmucndlem  20526  xmetunirn  20572  blbas  20665  blres  20666  mopnval  20673  setsmstopn  20713  tmsval  20716  tngtopn  20896  qtopbaslem  20997  xrtgioo  21043  reperflem  21055  icccmplem1  21059  reconnlem2  21064  xrge0tsms  21071  icopnfhmeo  21175  icccvx  21182  bndth  21190  reparphti  21229  pcofval  21242  pcoval1  21245  pcoval2  21248  pcoass  21256  pcorevlem  21258  pcorev2  21260  pi1xfrcnv  21289  nmhmcn  21335  csscld  21421  cfilfval  21435  caufval  21446  cfilres  21467  bcthlem1  21495  ivthlem1  21595  ivthlem3  21597  ovolicc2lem3  21662  ovolicc2lem4  21663  ioombl1lem4  21703  vitalilem1  21749  mbflimsup  21805  i1fima2  21818  i1fd  21820  i1f0  21826  i1f1  21829  itg1addlem4  21838  itg1addlem5  21839  itg2cnlem2  21901  iblmbf  21906  ellimc2  22013  limcres  22022  limcun  22031  dvbsss  22038  perfdvf  22039  dvres2lem  22046  dvaddbr  22073  rolle  22123  cmvth  22124  dvlip  22126  dvlipcn  22127  dvle  22140  lhop1lem  22146  dvfsumle  22154  dvfsumge  22155  dvfsumabs  22156  dvfsumlem2  22160  ftc2  22177  itgparts  22180  itgsubstlem  22181  itgsubst  22182  deg1mul3  22248  coeval  22352  coeeu  22354  dgrval  22357  coef3  22361  coemulc  22383  dgrsub  22400  coecj  22406  dvply2  22413  dvnply  22415  quotval  22419  fta1  22435  plyexmo  22440  aacjcl  22454  taylfval  22485  dvtaylp  22496  abelth  22567  pilem2  22578  pilem3  22579  sinord  22651  recosf1o  22652  resinf1o  22653  tanord1  22654  eff1olem  22665  dvloglem  22754  dvlog  22757  dvlog2lem  22758  advlogexp  22761  logtayl  22766  logtayl2  22768  cxpcn3lem  22846  cxpcn3  22847  sqrtcn  22849  loglesqrt  22857  1cubr  22898  acosrecl  22959  rlimcnp2  23021  xrlimcnp  23023  efrlim  23024  jensen  23043  basellem4  23082  ppiprm  23150  chtprm  23152  prmorcht  23177  dvdsflip  23183  musum  23192  chpchtsum  23219  dchrinvcl  23253  dchrghm  23256  dchrinv  23261  dchrsum2  23268  dchrsum  23269  rplogsumlem2  23395  rpvmasumlem  23397  dchrisum0re  23423  dchrisum0lem2a  23427  dirith2  23438  pnt  23524  tglng  23658  axlowdimlem5  23922  axlowdimlem6  23923  axlowdimlem7  23924  axlowdimlem15  23932  axlowdimlem16  23933  axlowdimlem17  23934  axlowdim  23937  axeuclidlem  23938  axcontlem2  23941  axcontlem7  23946  axcontlem8  23947  clwwlknprop  24445  clwwisshclww  24480  2wlkonot3v  24548  2spthonot3v  24549  issubgoi  24985  opidon  24997  flddivrng  25090  rngosn3  25101  vcoprnelem  25144  nvvcop  25160  nvex  25177  phnv  25402  sheli  25804  cheli  25823  choc1  25918  shintcli  25920  chintcli  25922  shsleji  25961  pjini  26290  mayete3i  26319  mayete3iOLD  26320  dmadjop  26480  nlelshi  26652  cnlnadjeui  26669  cnlnssadj  26672  bdopadj  26674  pjimai  26768  stcl  26808  atelch  26936  disjin  27116  fcnvgreu  27183  partfun  27185  f1od2  27216  fcobijfs  27218  xrge0infss  27245  iundisj2fi  27267  nnindf  27275  eliccioo  27292  xrsmulgzz  27325  xrge0mulgnn0  27336  xrge0nre  27339  xrge0omnd  27360  xrge0tsmsd  27435  prsdm  27529  prsrn  27530  ordtrestNEW  27536  xrge0iifcnv  27548  xrge0iifcv  27549  xrge0iifiso  27550  xrge0iifhom  27552  qqhcn  27605  qtophaus  27634  rnlogblem  27652  esumval  27694  gsumesum  27704  esumlub  27705  esumcst  27708  esumfsup  27713  issgon  27760  elrnsiga  27763  imambfm  27870  br2base  27877  sxbrsigalem0  27879  dya2iocucvr  27892  sxbrsigalem2  27894  sxbrsigalem5  27896  sxbrsiga  27898  sibfof  27919  oddpwdc  27930  eulerpartlemelr  27933  eulerpartgbij  27948  eulerpartlemgvv  27952  eulerpartlemgh  27954  eulerpartlemgs2  27956  eulerpartlemn  27957  sseqf  27968  ballotlem2  28064  ballotlemfp1  28067  ballotlemfc0  28068  ballotlemfcc  28069  ballotlemfmpn  28070  ballotlemsup  28080  ballotlemfrceq  28104  signswch  28155  lgamgulmlem2  28209  lgamucov2  28218  subfacp1lem5  28265  cvmsi  28347  divcnvshft  28591  zprod  28643  risefaccllem  28709  fallfaccllem  28710  dfon2lem4  28792  wfrlem4  28920  wfrlem10  28926  frrlem4  28964  pprodss4v  29108  linedegen  29367  bpolydiflem  29390  bpoly4  29395  nnssi2  29494  nnssi3  29495  sin2h  29620  cos2h  29621  tan2h  29622  heicant  29624  mblfinlem1  29626  cnambfre  29638  dvtan  29640  itg2addnc  29644  itg2gt0cn  29645  ftc1cnnc  29664  ftc2nc  29674  dvcncxp1  29675  dvcnsqrt  29676  dvasin  29678  dvacos  29679  ivthALT  29728  neibastop2lem  29779  cover2  29805  opelopab3  29808  sstotbnd2  29871  heibor1lem  29906  heiborlem10  29917  exidcl  29939  elrfi  30228  elrfirn  30229  elrfirn2  30230  mrefg3  30242  diophin  30308  diophun  30309  eq0rabdioph  30312  eqrabdioph  30313  pellex  30373  rmxycomplete  30455  rmxypos  30487  ltrmynn0  30488  jm2.23  30542  aomclem2  30605  fglmod  30623  lsmfgcl  30624  lmhmfgima  30634  lmhmfgsplit  30636  isnumbasabl  30659  dgrsub2  30688  itgocn  30718  acsfn1p  30753  areaquad  30789  eliccxr  31114  limcperiod  31170  sumnnodd  31172  limsupre  31183  limcresiooub  31184  limcresioolb  31185  limclner  31193  icccncfext  31226  fperdvper  31248  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgsin0pilem1  31267  itgsinexplem1  31271  itgsinexp  31272  ditgeqiooicc  31278  itgsubsticclem  31293  itgioocnicc  31295  itgsbtaddcnst  31300  stoweidlem34  31334  stoweidlem41  31341  stoweidlem51  31351  wallispilem2  31366  stirlinglem11  31384  dirkercncflem2  31404  fourierdlem5  31412  fourierdlem17  31424  fourierdlem18  31425  fourierdlem20  31427  fourierdlem25  31432  fourierdlem39  31446  fourierdlem40  31447  fourierdlem42  31449  fourierdlem48  31455  fourierdlem56  31463  fourierdlem57  31464  fourierdlem58  31465  fourierdlem60  31467  fourierdlem61  31468  fourierdlem62  31469  fourierdlem64  31471  fourierdlem66  31473  fourierdlem68  31475  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem79  31486  fourierdlem81  31488  fourierdlem83  31490  fourierdlem85  31492  fourierdlem88  31495  fourierdlem89  31496  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem95  31502  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  sqwvfourb  31530  fouriersw  31532  onfrALTlem2  32398  onfrALTlem2VD  32769  bnj1533  32989  bnj1137  33130  bnj1286  33154  bnj1408  33171  bnj1417  33176  bj-sngltagi  33621  bj-elid  33672  bj-elid2  33673  bj-flbi3  33679  bj-cmnssmndel  33725  bj-ablssgrpel  33727  bj-ablsscmnel  33729  bj-vecssmodel  33732  bj-rrvecssvecel  33739  bj-rrvecsscmnel  33741  toycom  33770  osumcllem7N  34758  pexmidlem4N  34769  diaintclN  35855  dibintclN  35964  mapd1o  36445  hdmapevec  36635  taupilemrplb  36766  fiinfi  36778
  Copyright terms: Public domain W3C validator