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

Theorem sseli 3940
Description: Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sseli.1 𝐴𝐵
Assertion
Ref Expression
sseli (𝐶𝐴𝐶𝐵)

Proof of Theorem sseli
StepHypRef Expression
1 sseli.1 . 2 𝐴𝐵
2 ssel 3937 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927
This theorem is referenced by:  sselii  3941  sselid  3942  elun1  4136  elun2  4137  elopabr  5518  elopabran  5519  elopaelxp  5721  copsex2ga  5763  2elresin  6622  nfvres  6883  fvco4i  6942  mptrcl  6957  fvmptss  6960  fvmptex  6962  fvmptnf  6970  elfvmptrab1w  6974  elfvmptrab1  6975  fvopab4ndm  6977  fvimacnvi  7002  elpreima  7008  iinpreima  7019  ofrfvalg  7625  ofval  7628  off  7635  nnon  7808  finds  7835  finds2  7837  eqopi  7957  op1steq  7965  dfoprab4  7987  bropopvvv  8022  bropfvvvv  8024  reldmtpos  8165  wfrlem10OLD  8264  smores2  8300  frsuc  8383  nnfiOLD  9176  unifpw  9299  cantnfp1lem1  9614  cantnfp1lem3  9616  r1fin  9709  r1tr  9712  r1ordg  9714  r1ord3g  9715  r1val1  9722  tz9.12lem3  9725  tcrank  9820  cplem1  9825  hta  9833  tskwe  9886  cardprclem  9915  alephfplem3  10042  dfac12r  10082  ackbij1lem16  10171  ackbij2  10179  fin23lem28  10276  fin23lem30  10278  fin23lem31  10279  fin1a2lem6  10341  hsmexlem4  10365  hsmexlem5  10366  hsmexlem6  10367  axdc2lem  10384  axdc3lem2  10387  axcclem  10393  brdom5  10465  brdom4  10466  r1tskina  10718  gruina  10754  grur1a  10755  pinn  10814  0nnq  10860  elpqn  10861  recn  11141  rexr  11201  ltord1  11681  leord1  11682  eqord1  11683  nnre  12160  nncn  12161  nnind  12171  nnnn0  12420  nn0re  12422  nn0cn  12423  nn0xnn0  12489  nnzOLD  12523  nn0z  12524  nnq  12887  qcn  12888  rpre  12923  eliccxr  13352  difreicc  13401  iccshftri  13404  iccshftli  13406  iccdili  13408  icccntri  13410  fzval2  13427  fzelp1  13493  4fvwrd4  13561  elfzo1  13622  ico01fl0  13724  expcllem  13978  expcl2lem  13979  m1expcl2  13991  bcm1k  14215  bcpasc  14221  hashbclem  14349  wrdv  14417  pfxfv0  14580  pfxfvlsw  14583  cshimadifsn  14718  swrds2m  14830  01sqrexlem5  15131  cau3lem  15239  caubnd  15243  climconst2  15430  o1of2  15495  o1rlimmul  15501  caurcvg  15561  caucvg  15563  binomlem  15714  incexclem  15721  divcnvshft  15740  zprod  15820  fprodge1  15878  risefaccllem  15896  fallfaccllem  15897  bpolydiflem  15937  bpoly4  15942  dvdsflip  16199  divalglem8  16282  sadadd  16347  smumul  16373  isprm3  16559  phimullem  16651  prmdiveq  16658  unbenlem  16780  vdwnnlem1  16867  vdwnnlem3  16869  ramtcl2  16883  prmgaplem4  16926  cshwshashlem1  16968  structcnvcnv  17025  fvsetsid  17040  imasdsval2  17398  mreunirn  17481  mrcfval  17488  mrisval  17510  coapm  17957  tsrss  18478  submnd0  18585  smndex1id  18721  nmzsubg  18967  nmznsg  18970  cntzmhm  19119  symgtrinv  19254  pmtrdifellem4  19261  psgnpmtr  19292  efginvrel2  19509  efginvrel1  19510  efgsp1  19519  efgsres  19520  efgsfo  19521  frgpinv  19546  frgpupf  19555  frgpup1  19557  subcmn  19615  torsubg  19632  dprd2dlem1  19820  dpjidcl  19837  ablfaclem3  19866  acsfn1p  20266  lssacs  20428  cnsubdrglem  20848  rege0subm  20853  rge0srg  20868  zringunit  20887  znrrg  20972  psgnghm  20984  zrhpsgnevpm  20995  evpmodpmf1o  21000  pmtrodpm  21001  phlssphl  21063  frlmsslsp  21202  islinds4  21241  lmimlbs  21242  lbslcic  21247  psrbaglefi  21334  psrbaglefiOLD  21335  psrbagconf1o  21338  mplsubglem  21405  mplneg  21414  ressmpladd  21430  ressmplmul  21431  ressmplvsca  21432  mplmonmul  21437  ply1bascl  21574  mdetralt  21957  mdetunilem7  21967  chfacfpmmulgsum2  22214  tgval2  22306  ordtbas  22543  ordtrestixx  22573  hauslly  22843  kgentop  22893  ptbasin  22928  filunirn  23233  uzrest  23248  elflim  23322  flffval  23340  fclsval  23359  isfcls  23360  fcfval  23384  ustn0  23572  fmucndlem  23643  xmetunirn  23690  mopnval  23791  setsmstopn  23833  tmsval  23836  tngtopn  24014  qtopbaslem  24122  xrtgioo  24169  reperflem  24181  icccmplem1  24185  icopnfhmeo  24306  icccvx  24313  bndth  24321  reparphti  24360  pcoval1  24376  pcoval2  24379  pcoass  24387  pcorevlem  24389  pcorev2  24391  pi1xfrcnv  24420  csscld  24613  cfilfval  24628  caufval  24639  bcthlem1  24688  ivthlem1  24815  ivthlem3  24817  ovolicc2lem3  24883  ovolicc2lem4  24884  vitalilem1  24972  mbflimsup  25030  i1fd  25045  i1f0  25051  i1f1  25054  itg1addlem4  25063  itg1addlem4OLD  25064  itg1addlem5  25065  iblmbf  25132  ellimc2  25241  limcres  25250  limcun  25259  dvbsss  25266  perfdvf  25267  dvres2lem  25274  dvaddbr  25302  rolle  25354  cmvth  25355  dvlip  25357  dvlipcn  25358  dvle  25371  lhop1lem  25377  dvfsumle  25385  dvfsumge  25386  dvfsumabs  25387  dvfsumlem2  25391  ftc2  25408  itgparts  25411  itgsubstlem  25412  itgsubst  25413  deg1mul3  25480  coeval  25584  coeeu  25586  dgrval  25589  coef3  25593  coemulc  25616  dgrsub  25633  coecj  25639  dvply2  25646  dvnply  25648  quotval  25652  fta1  25668  plyexmo  25673  aacjcl  25687  taylfval  25718  dvtaylp  25729  abelth  25800  pilem3  25812  cos0pilt1  25888  sinord  25890  recosf1o  25891  resinf1o  25892  tanord1  25893  eff1olem  25904  dvloglem  26003  dvlog  26006  dvlog2lem  26007  advlogexp  26010  logtayl  26015  logtayl2  26017  dvcncxp1  26096  dvcnsqrt  26097  cxpcn3lem  26100  cxpcn3  26101  sqrtcn  26103  loglesqrt  26111  1cubr  26192  acosrecl  26253  efrlim  26319  jensen  26338  lgamgulmlem2  26379  lgamucov2  26388  basellem4  26433  musum  26540  dchrinvcl  26601  dchrghm  26604  dchrinv  26609  dchrsum2  26616  dchrsum  26617  rpvmasumlem  26835  dchrisum0lem2a  26865  pnt  26962  oldf  27187  leftirr  27220  rightirr  27221  lrold  27226  sltlpss  27236  addsproplem2  27282  sleadd1  27298  addsunif  27310  negsproplem2  27327  negsid  27339  negsunif  27350  tglng  27488  axlowdimlem6  27896  axlowdimlem16  27906  axlowdimlem17  27907  axlowdim  27910  axeuclidlem  27911  axcontlem2  27914  axcontlem7  27919  axcontlem8  27920  nbusgrvtxm1uvtx  28353  wlk1walk  28587  pthdivtx  28677  pthdadjvtx  28678  crctcshwlkn0lem2  28756  crctcshwlkn0lem4  28758  clwwisshclwws  28959  fusgreg2wsp  29280  nvvcop  29536  nvex  29553  phnv  29756  sheli  30156  cheli  30174  hhssabloilem  30203  choc1  30269  shintcli  30271  chintcli  30273  shsleji  30312  pjini  30641  mayete3i  30670  dmadjop  30830  nlelshi  31002  cnlnadjeui  31019  cnlnssadj  31022  bdopadj  31024  pjimai  31118  stcl  31158  atelch  31286  fcnvgreu  31589  f1od2  31638  fcobijfs  31640  uzssico  31687  iundisj2fi  31700  nnindf  31715  eliccioo  31787  gsummptres  31894  cyc3genpm  32001  elrspunidl  32203  zarcls  32455  ordtrestNEW  32502  xrge0iifcnv  32514  xrge0iifcv  32515  xrge0iifiso  32516  xrge0iifhom  32518  qqhcn  32572  esumval  32645  gsumesum  32658  esumlub  32659  esumcst  32662  esumfsup  32669  issgon  32722  elrnsiga  32725  imambfm  32862  br2base  32869  sxbrsigalem0  32871  dya2iocucvr  32884  sxbrsigalem2  32886  sxbrsigalem5  32888  sxbrsiga  32890  omssubadd  32900  sitmcl  32951  oddpwdc  32954  eulerpartlemelr  32957  eulerpartlemgvv  32976  eulerpartlemgh  32978  eulerpartlemgs2  32980  eulerpartlemn  32981  sseqf  32992  ballotlem2  33088  ballotlemfp1  33091  ballotlemfc0  33092  ballotlemfcc  33093  ballotlemfmpn  33094  ballotlemsup  33104  ballotlemfrceq  33128  signswch  33173  rpsqrtcn  33206  prodfzo03  33216  itgexpif  33219  bnj1533  33464  bnj1137  33607  bnj1286  33631  bnj1408  33648  bnj1417  33653  subfacp1lem5  33778  cvmsi  33859  gonar  33989  goalr  33991  mpst123  34134  mpstrcl  34135  msrrcl  34137  elmsta  34142  msubvrs  34154  elmpps  34167  elmthm  34170  bcprod  34311  dfon2lem4  34361  mulsid1  34411  mulsid2  34412  pprodss4v  34469  ivthALT  34807  neibastop2lem  34832  nnssi2  34927  nnssi3  34928  bj-sngltagi  35453  bj-elid5  35640  bj-fvmptunsn1  35728  bj-smgrpssmgmel  35740  bj-mndsssmgrpel  35742  bj-cmnssmndel  35744  bj-grpssmndel  35746  bj-ablssgrpel  35748  bj-ablsscmnel  35750  bj-vecssmodel  35753  bj-flddrng  35760  bj-rveccvec  35776  bj-rvecabl  35778  taupilemrplb  35791  icorempo  35822  elxp8  35842  sin2h  36068  cos2h  36069  tan2h  36070  poimirlem14  36092  poimirlem26  36104  poimirlem27  36105  poimirlem31  36109  poimirlem32  36110  mblfinlem1  36115  cnambfre  36126  dvtan  36128  itg2addnc  36132  itg2gt0cn  36133  ftc1cnnc  36150  ftc2nc  36160  dvasin  36162  dvacos  36163  cover2  36173  sstotbnd2  36233  heibor1lem  36268  heiborlem10  36279  opidonOLD  36311  exidcl  36335  rngosn3  36383  flddivrng  36458  toycom  37435  osumcllem7N  38425  pexmidlem4N  38436  diaintclN  39521  dibintclN  39630  mapd1o  40111  hdmapevec  40298  dvrelog2  40521  sticksstones1  40554  rncrhmcl  40694  prjspvs  40934  prjspeclsp  40936  0prjspnrel  40951  elrfi  41003  elrfirn  41004  elrfirn2  41005  mrefg3  41017  diophin  41081  diophun  41082  eq0rabdioph  41085  eqrabdioph  41086  pellex  41144  rmxycomplete  41227  jm2.23  41306  aomclem2  41368  fglmod  41386  lsmfgcl  41387  lmhmfgima  41397  lmhmfgsplit  41399  isnumbasabl  41419  dgrsub2  41448  itgocn  41477  areaquad  41536  cantnftermord  41640  omabs2  41651  nna1iscard  41807  elmapintrab  41838  corcltrcl  42001  k0004val0  42416  elscottab  42514  radcnvrat  42584  uzmptshftfval  42616  binomcxplemdvsum  42625  binomcxplemnotnn0  42626  onfrALTlem2  42818  onfrALTlem2VD  43161  uzwo4  43251  mptssid  43457  uzublem  43655  eliccelioc  43749  elicores  43761  sqrlearg  43781  fsumiunss  43806  limcdm0  43849  sumnnodd  43861  fnlimfvre  43905  limsupubuzlem  43943  limsupmnflem  43951  limsupre3uzlem  43966  climuzlem  43974  cncfshift  44105  cncfperiod  44110  icccncfext  44118  dvnprodlem1  44177  dvnprodlem2  44178  itgsin0pilem1  44181  itgsinexplem1  44185  itgsinexp  44186  ditgeqiooicc  44191  itgsubsticclem  44206  itgioocnicc  44208  itgsbtaddcnst  44213  stoweidlem34  44265  stoweidlem41  44272  stoweidlem51  44282  wallispilem2  44297  stirlinglem11  44315  dirkercncflem2  44335  fourierdlem5  44343  fourierdlem9  44347  fourierdlem17  44355  fourierdlem18  44356  fourierdlem20  44358  fourierdlem39  44377  fourierdlem48  44385  fourierdlem49  44386  fourierdlem62  44399  fourierdlem66  44403  fourierdlem68  44405  fourierdlem72  44409  fourierdlem73  44410  fourierdlem81  44418  fourierdlem83  44420  fourierdlem85  44422  fourierdlem87  44424  fourierdlem88  44425  fourierdlem92  44429  fourierdlem95  44432  fourierdlem103  44440  fourierdlem104  44441  fourierdlem112  44449  sqwvfoura  44459  sqwvfourb  44460  fouriersw  44462  etransclem24  44489  etransclem35  44500  etransclem37  44502  salexct  44565  salgencntex  44574  sge0resplit  44637  sge0split  44640  meaiuninclem  44711  caratheodorylem1  44757  volicorescl  44784  hoidmv1lelem3  44824  opnvonmbllem2  44864  ovolval2  44875  ovolval3  44878  ovolval4lem1  44880  ovolval4lem2  44881  pimiooltgt  44941  sssmf  44969  smfaddlem1  44994  smflimlem2  45003  smfrec  45020  smfdiv  45028  smfsuplem1  45042  smfsuplem3  45044  et-ltneverrefl  45102  natglobalincr  45106  fcores  45291  spr0el  45664  bgoldbtbndlem2  45988  bgoldbtbndlem3  45989  bgoldbtbnd  45991  fldhmsubc  46372  fldhmsubcALTV  46390  fvconst0ci  46915  fvconstdomi  46916
  Copyright terms: Public domain W3C validator