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

Theorem sseli 3413
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 3411 . 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 1826    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  sselii  3414  sseldi  3415  elun1  3585  elun2  3586  copsex2ga  5027  issref  5293  2elresin  5600  nfvres  5804  fvco4i  5852  mptrcl  5863  fvmptss  5866  fvmptex  5868  fvmptnf  5875  elfvmptrab1  5878  fvopab4ndm  5880  fvimacnvi  5903  elpreima  5909  iinpreima  5919  ofrfval  6447  ofval  6448  off  6453  nnon  6605  finds  6625  finds2  6627  offres  6694  eqopi  6733  op1steq  6741  dfoprab4  6756  bropopvvv  6779  curry1val  6792  curry2val  6796  reldmtpos  6881  smores3  6942  smores2  6943  frsuc  7020  nnfi  7629  unifpw  7738  f1opwfi  7739  fival  7787  fi0  7795  dffi2  7798  elfiun  7805  cantnfp1lem1  8010  cantnfp1lem3  8012  cantnfp1lem1OLD  8036  cantnfp1lem3OLD  8038  epfrs  8075  r1fin  8104  r1tr  8107  r1ordg  8109  r1ord3g  8110  r1val1  8117  tz9.12lem3  8120  tcrank  8215  cplem1  8220  hta  8228  tskwe  8244  cardprclem  8273  r0weon  8303  fodomfi2  8354  alephfplem3  8400  dfac12r  8439  ackbij1lem6  8518  ackbij1lem9  8521  ackbij1lem10  8522  ackbij1lem11  8523  ackbij1lem16  8528  ackbij1lem18  8530  ackbij2  8536  fin23lem24  8615  fin23lem26  8618  fin23lem28  8633  fin23lem30  8635  fin23lem31  8636  isfin1-3  8679  fin1a2lem6  8698  hsmexlem4  8722  hsmexlem5  8723  hsmexlem6  8724  axdc2lem  8741  axdc3lem2  8744  axcclem  8750  ac6num  8772  brdom5  8820  brdom4  8821  canthp1lem2  8942  r1tskina  9071  gruina  9107  grur1a  9108  pinn  9167  0nnq  9213  elpqn  9214  recn  9493  rexr  9550  dedekindle  9656  ltord1  9996  leord1  9997  eqord1  9998  nnre  10459  nncn  10460  nnind  10470  nnnn0  10719  nn0re  10721  nn0cn  10722  nnz  10803  nn0z  10804  nnq  11114  qcn  11115  rpre  11145  difreicc  11573  iccshftri  11576  iccshftli  11578  iccdili  11580  icccntri  11582  fzval2  11596  fzelp1  11654  4fvwrd4  11715  elfzo1  11766  ico01fl0  11853  expcllem  12080  expcl2lem  12081  m1expcl2  12091  bcm1k  12295  bcpasc  12301  hashbclem  12405  swrd0fv0  12576  swrd0fvlsw  12579  sqrlem5  13082  cau3lem  13189  caubnd  13193  climconst2  13373  rlimres  13383  lo1res  13384  lo1resb  13389  rlimresb  13390  o1resb  13391  o1of2  13437  o1rlimmul  13443  caurcvg  13501  caucvg  13503  ackbijnn  13642  binomlem  13643  incexclem  13650  zprod  13746  divalglem8  14060  sadadd  14119  smueqlem  14142  smumul  14145  isprm3  14228  phimullem  14311  prmdiveq  14318  unbenlem  14428  prmreclem2  14437  prmrec  14442  vdwnnlem1  14515  vdwnnlem3  14517  ramtcl2  14531  cshwshashlem1  14582  isstruct2  14643  structcnvcnv  14645  fvsetsid  14661  strlemor1  14729  imasdsval2  14923  xpsfrnel2  14972  mreunirn  15008  mrcfval  15015  mrisval  15037  isacs2  15060  acsfn  15066  homarcl  15424  arwval  15439  coafval  15460  coapm  15467  isdrs2  15685  isacs3lem  15913  psssdm2  15962  tsrss  15970  submnd0  16067  nmzsubg  16359  nmznsg  16362  resscntz  16486  cntzmhm  16493  symgtrinv  16614  pmtrdifellem4  16621  psgnpmtr  16652  efginvrel2  16862  efginvrel1  16863  efgsp1  16872  efgsres  16873  efgsfo  16874  frgpinv  16899  frgpupf  16908  frgpup1  16910  subcmn  16962  torsubg  16977  dprd2dlem1  17203  dpjidcl  17220  dpjidclOLD  17227  ablfaclem3  17251  subrgpropd  17576  lssacs  17726  sralmod  17946  psrbaglefi  18136  psrbaglefiOLD  18137  mplsubglem  18206  mplsubglemOLD  18208  ressmpladd  18232  ressmplmul  18233  ressmplvsca  18234  mplmonmul  18239  mplind  18280  ply1bascl  18355  cnsubdrglem  18582  rege0subm  18587  rge0srg  18600  zringunit  18621  znrrg  18695  psgnghm  18707  zrhpsgnevpm  18718  evpmodpmf1o  18723  pmtrodpm  18724  frlmsslsp  18916  islinds4  18955  lmimlbs  18956  lbslcic  18961  mdetralt  19195  mdetunilem7  19205  chfacfpmmulgsum2  19451  basdif0  19539  tgval2  19542  mreclatdemoBAD  19683  ordtbas  19779  ordtrest  19789  ordtrestixx  19809  fincmp  19979  cmpfi  19994  bwth  19996  iuncon  20014  1stcrest  20039  hauslly  20078  kgentop  20128  ptbasin  20163  ptcnplem  20207  txkgen  20238  infil  20449  filunirn  20468  uzrest  20483  elflim  20557  hauspwpwf1  20573  flffval  20575  fclsval  20594  isfcls  20595  fcfval  20619  alexsubALTlem3  20634  alexsubALTlem4  20635  ustn0  20808  fmucndlem  20879  xmetunirn  20925  blbas  21018  blres  21019  mopnval  21026  setsmstopn  21066  tmsval  21069  tngtopn  21249  qtopbaslem  21350  xrtgioo  21396  reperflem  21408  icccmplem1  21412  reconnlem2  21417  xrge0tsms  21424  icopnfhmeo  21528  icccvx  21535  bndth  21543  reparphti  21582  pcofval  21595  pcoval1  21598  pcoval2  21601  pcoass  21609  pcorevlem  21611  pcorev2  21613  pi1xfrcnv  21642  nmhmcn  21688  csscld  21774  cfilfval  21788  caufval  21799  cfilres  21820  bcthlem1  21848  ivthlem1  21948  ivthlem3  21950  ovolicc2lem3  22015  ovolicc2lem4  22016  ioombl1lem4  22056  vitalilem1  22102  mbflimsup  22158  i1fima2  22171  i1fd  22173  i1f0  22179  i1f1  22182  itg1addlem4  22191  itg1addlem5  22192  itg2cnlem2  22254  iblmbf  22259  ellimc2  22366  limcres  22375  limcun  22384  dvbsss  22391  perfdvf  22392  dvres2lem  22399  dvaddbr  22426  rolle  22476  cmvth  22477  dvlip  22479  dvlipcn  22480  dvle  22493  lhop1lem  22499  dvfsumle  22507  dvfsumge  22508  dvfsumabs  22509  dvfsumlem2  22513  ftc2  22530  itgparts  22533  itgsubstlem  22534  itgsubst  22535  deg1mul3  22601  coeval  22705  coeeu  22707  dgrval  22710  coef3  22714  coemulc  22737  dgrsub  22754  coecj  22760  dvply2  22767  dvnply  22769  quotval  22773  fta1  22789  plyexmo  22794  aacjcl  22808  taylfval  22839  dvtaylp  22850  abelth  22921  pilem2  22932  pilem3  22933  sinord  23006  recosf1o  23007  resinf1o  23008  tanord1  23009  eff1olem  23020  dvloglem  23116  dvlog  23119  dvlog2lem  23120  advlogexp  23123  logtayl  23128  logtayl2  23130  cxpcn3lem  23208  cxpcn3  23209  sqrtcn  23211  loglesqrt  23219  1cubr  23289  acosrecl  23350  rlimcnp2  23413  xrlimcnp  23415  efrlim  23416  jensen  23435  basellem4  23474  ppiprm  23542  chtprm  23544  prmorcht  23569  dvdsflip  23575  musum  23584  chpchtsum  23611  dchrinvcl  23645  dchrghm  23648  dchrinv  23653  dchrsum2  23660  dchrsum  23661  rplogsumlem2  23787  rpvmasumlem  23789  dchrisum0re  23815  dchrisum0lem2a  23819  dirith2  23830  pnt  23916  tglng  24053  axlowdimlem6  24371  axlowdimlem16  24381  axlowdimlem17  24382  axlowdim  24385  axeuclidlem  24386  axcontlem2  24389  axcontlem7  24394  axcontlem8  24395  clwwlknprop  24893  clwwisshclww  24928  2wlkonot3v  24996  2spthonot3v  24997  issubgoi  25429  opidonOLD  25441  flddivrng  25534  rngosn3  25545  vcoprnelem  25588  nvvcop  25604  nvex  25621  phnv  25846  sheli  26248  cheli  26267  choc1  26362  shintcli  26364  chintcli  26366  shsleji  26405  pjini  26734  mayete3i  26763  dmadjop  26923  nlelshi  27095  cnlnadjeui  27112  cnlnssadj  27115  bdopadj  27117  pjimai  27211  stcl  27251  atelch  27379  disjin  27576  fcnvgreu  27660  partfun  27663  f1od2  27697  fcobijfs  27699  xrge0infss  27730  iundisj2fi  27755  nnindf  27763  eliccioo  27780  xrge0mulgnn0  27830  xrge0nre  27833  xrge0omnd  27854  xrge0tsmsd  27929  prsdm  28050  prsrn  28051  ordtrestNEW  28057  xrge0iifcnv  28069  xrge0iifcv  28070  xrge0iifiso  28071  xrge0iifhom  28073  qqhcn  28125  esumval  28194  gsumesum  28207  esumlub  28208  esumcst  28211  esumfsup  28218  esumcvgre  28239  issgon  28272  elrnsiga  28275  imambfm  28389  br2base  28396  sxbrsigalem0  28398  dya2iocucvr  28411  sxbrsigalem2  28413  sxbrsigalem5  28415  sxbrsiga  28417  omssubadd  28427  oddpwdc  28476  eulerpartlemelr  28479  eulerpartgbij  28494  eulerpartlemgvv  28498  eulerpartlemgh  28500  eulerpartlemgs2  28502  eulerpartlemn  28503  sseqf  28514  ballotlem2  28610  ballotlemfp1  28613  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemfmpn  28616  ballotlemsup  28626  ballotlemfrceq  28650  signswch  28701  lgamgulmlem2  28761  lgamucov2  28770  subfacp1lem5  28817  cvmsi  28899  mpst123  29089  mpstrcl  29090  msrrcl  29092  elmsta  29097  msubvrs  29109  elmpps  29122  elmthm  29125  divcnvshft  29283  risefaccllem  29301  fallfaccllem  29302  dfon2lem4  29383  wfrlem4  29511  wfrlem10  29517  frrlem4  29555  pprodss4v  29687  bpolydiflem  29969  bpoly4  29974  nnssi2  30073  nnssi3  30074  sin2h  30210  cos2h  30211  tan2h  30212  heicant  30214  mblfinlem1  30216  cnambfre  30228  dvtan  30231  itg2addnc  30235  itg2gt0cn  30236  ftc1cnnc  30255  ftc2nc  30265  dvcncxp1  30266  dvcnsqrt  30267  dvasin  30269  dvacos  30270  ivthALT  30319  neibastop2lem  30344  cover2  30370  sstotbnd2  30436  heibor1lem  30471  heiborlem10  30482  exidcl  30504  elrfi  30792  elrfirn  30793  elrfirn2  30794  mrefg3  30806  diophin  30871  diophun  30872  eq0rabdioph  30875  eqrabdioph  30876  pellex  30936  rmxycomplete  31018  jm2.23  31104  aomclem2  31167  fglmod  31185  lsmfgcl  31186  lmhmfgima  31196  lmhmfgsplit  31198  isnumbasabl  31223  dgrsub2  31252  itgocn  31281  acsfn1p  31316  areaquad  31352  radcnvrat  31363  uzmptshftfval  31419  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  eliccxr  31716  eliccelioc  31727  fprodge1  31764  limcdm0  31790  sumnnodd  31802  cncfshift  31842  cncfperiod  31847  icccncfext  31856  dvnprodlem1  31909  dvnprodlem2  31910  itgsin0pilem1  31914  itgsinexplem1  31918  itgsinexp  31919  ditgeqiooicc  31925  itgsubsticclem  31940  itgioocnicc  31942  itgsbtaddcnst  31947  stoweidlem34  31982  stoweidlem41  31989  stoweidlem51  31999  wallispilem2  32014  stirlinglem11  32032  dirkercncflem2  32052  fourierdlem5  32060  fourierdlem9  32064  fourierdlem17  32072  fourierdlem18  32073  fourierdlem20  32075  fourierdlem39  32094  fourierdlem48  32103  fourierdlem49  32104  fourierdlem62  32117  fourierdlem66  32121  fourierdlem68  32123  fourierdlem72  32127  fourierdlem73  32128  fourierdlem81  32136  fourierdlem83  32138  fourierdlem85  32140  fourierdlem87  32142  fourierdlem88  32143  fourierdlem92  32147  fourierdlem95  32150  fourierdlem103  32158  fourierdlem104  32159  fourierdlem112  32167  sqwvfoura  32177  sqwvfourb  32178  fouriersw  32180  etransclem24  32207  etransclem35  32218  etransclem37  32220  pfxfv0  32575  pfxfvlsw  32578  fldhmsubc  33092  fldhmsubcALTV  33111  onfrALTlem2  33658  onfrALTlem2VD  34036  bnj1533  34257  bnj1137  34398  bnj1286  34422  bnj1408  34439  bnj1417  34444  bj-sngltagi  34888  bj-elid  34947  bj-elid2  34948  bj-cmnssmndel  35000  bj-ablssgrpel  35002  bj-ablsscmnel  35004  bj-vecssmodel  35007  bj-rrvecssvecel  35014  bj-rrvecsscmnel  35016  toycom  35111  osumcllem7N  36099  pexmidlem4N  36110  diaintclN  37198  dibintclN  37307  mapd1o  37788  hdmapevec  37978  taupilemrplb  38108  fiinfi  38187  corcltrcl  38249
  Copyright terms: Public domain W3C validator