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

Theorem sseli 3911
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 3908 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wss 3881
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898
This theorem is referenced by:  sselii  3912  sseldi  3913  elun1  4103  elun2  4104  elopabran  5413  copsex2ga  5644  2elresin  6440  nfvres  6681  fvco4i  6739  mptrcl  6754  fvmptss  6757  fvmptex  6759  fvmptnf  6767  elfvmptrab1w  6771  elfvmptrab1  6772  fvopab4ndm  6774  fvimacnvi  6799  elpreima  6805  iinpreima  6814  ofrfval  7397  ofval  7398  off  7404  nnon  7566  finds  7589  finds2  7591  eqopi  7707  op1steq  7715  dfoprab4  7735  bropopvvv  7768  bropfvvvv  7770  reldmtpos  7883  wfrlem10  7947  smores2  7974  frsuc  8055  nnfi  8696  unifpw  8811  cantnfp1lem1  9125  cantnfp1lem3  9127  r1fin  9186  r1tr  9189  r1ordg  9191  r1ord3g  9192  r1val1  9199  tz9.12lem3  9202  tcrank  9297  cplem1  9302  hta  9310  tskwe  9363  cardprclem  9392  alephfplem3  9517  dfac12r  9557  ackbij1lem16  9646  ackbij2  9654  fin23lem28  9751  fin23lem30  9753  fin23lem31  9754  fin1a2lem6  9816  hsmexlem4  9840  hsmexlem5  9841  hsmexlem6  9842  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  ac6num  9890  brdom5  9940  brdom4  9941  r1tskina  10193  gruina  10229  grur1a  10230  pinn  10289  0nnq  10335  elpqn  10336  recn  10616  rexr  10676  ltord1  11155  leord1  11156  eqord1  11157  nnre  11632  nncn  11633  nnind  11643  nnnn0  11892  nn0re  11894  nn0cn  11895  nn0xnn0  11959  nnz  11992  nn0z  11993  nnq  12349  qcn  12350  rpre  12385  eliccxr  12813  difreicc  12862  iccshftri  12865  iccshftli  12867  iccdili  12869  icccntri  12871  fzval2  12888  fzelp1  12954  4fvwrd4  13022  elfzo1  13082  ico01fl0  13184  expcllem  13436  expcl2lem  13437  m1expcl2  13447  bcm1k  13671  bcpasc  13677  hashbclem  13806  wrdv  13872  pfxfv0  14045  pfxfvlsw  14048  cshimadifsn  14182  swrds2m  14294  sqrlem5  14598  cau3lem  14706  caubnd  14710  climconst2  14897  o1of2  14961  o1rlimmul  14967  caurcvg  15025  caucvg  15027  binomlem  15176  incexclem  15183  divcnvshft  15202  zprod  15283  fprodge1  15341  risefaccllem  15359  fallfaccllem  15360  bpolydiflem  15400  bpoly4  15405  dvdsflip  15659  divalglem8  15741  sadadd  15806  smumul  15832  isprm3  16017  phimullem  16106  prmdiveq  16113  unbenlem  16234  vdwnnlem1  16321  vdwnnlem3  16323  ramtcl2  16337  prmgaplem4  16380  cshwshashlem1  16421  structcnvcnv  16489  fvsetsid  16507  imasdsval2  16781  mreunirn  16864  mrcfval  16871  mrisval  16893  coapm  17323  tsrss  17825  submnd0  17932  smndex1id  18068  nmzsubg  18309  nmznsg  18312  cntzmhm  18461  symgtrinv  18592  pmtrdifellem4  18599  psgnpmtr  18630  efginvrel2  18845  efginvrel1  18846  efgsp1  18855  efgsres  18856  efgsfo  18857  frgpinv  18882  frgpupf  18891  frgpup1  18893  subcmn  18950  torsubg  18967  dprd2dlem1  19156  dpjidcl  19173  ablfaclem3  19202  acsfn1p  19571  lssacs  19732  cnsubdrglem  20142  rege0subm  20147  rge0srg  20162  zringunit  20181  znrrg  20257  psgnghm  20269  zrhpsgnevpm  20280  evpmodpmf1o  20285  pmtrodpm  20286  phlssphl  20348  frlmsslsp  20485  islinds4  20524  lmimlbs  20525  lbslcic  20530  psrbaglefi  20610  mplsubglem  20672  mplneg  20681  ressmpladd  20697  ressmplmul  20698  ressmplvsca  20699  mplmonmul  20704  ply1bascl  20832  mdetralt  21213  mdetunilem7  21223  chfacfpmmulgsum2  21470  tgval2  21561  ordtbas  21797  ordtrestixx  21827  hauslly  22097  kgentop  22147  ptbasin  22182  filunirn  22487  uzrest  22502  elflim  22576  flffval  22594  fclsval  22613  isfcls  22614  fcfval  22638  ustn0  22826  fmucndlem  22897  xmetunirn  22944  mopnval  23045  setsmstopn  23085  tmsval  23088  tngtopn  23256  qtopbaslem  23364  xrtgioo  23411  reperflem  23423  icccmplem1  23427  icopnfhmeo  23548  icccvx  23555  bndth  23563  reparphti  23602  pcoval1  23618  pcoval2  23621  pcoass  23629  pcorevlem  23631  pcorev2  23633  pi1xfrcnv  23662  csscld  23853  cfilfval  23868  caufval  23879  bcthlem1  23928  ivthlem1  24055  ivthlem3  24057  ovolicc2lem3  24123  ovolicc2lem4  24124  vitalilem1  24212  mbflimsup  24270  i1fd  24285  i1f0  24291  i1f1  24294  itg1addlem4  24303  itg1addlem5  24304  iblmbf  24371  ellimc2  24480  limcres  24489  limcun  24498  dvbsss  24505  perfdvf  24506  dvres2lem  24513  dvaddbr  24541  rolle  24593  cmvth  24594  dvlip  24596  dvlipcn  24597  dvle  24610  lhop1lem  24616  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvfsumlem2  24630  ftc2  24647  itgparts  24650  itgsubstlem  24651  itgsubst  24652  deg1mul3  24716  coeval  24820  coeeu  24822  dgrval  24825  coef3  24829  coemulc  24852  dgrsub  24869  coecj  24875  dvply2  24882  dvnply  24884  quotval  24888  fta1  24904  plyexmo  24909  aacjcl  24923  taylfval  24954  dvtaylp  24965  abelth  25036  pilem3  25048  cos0pilt1  25124  sinord  25126  recosf1o  25127  resinf1o  25128  tanord1  25129  eff1olem  25140  dvloglem  25239  dvlog  25242  dvlog2lem  25243  advlogexp  25246  logtayl  25251  logtayl2  25253  dvcncxp1  25332  dvcnsqrt  25333  cxpcn3lem  25336  cxpcn3  25337  sqrtcn  25339  loglesqrt  25347  1cubr  25428  acosrecl  25489  efrlim  25555  jensen  25574  lgamgulmlem2  25615  lgamucov2  25624  basellem4  25669  musum  25776  dchrinvcl  25837  dchrghm  25840  dchrinv  25845  dchrsum2  25852  dchrsum  25853  rpvmasumlem  26071  dchrisum0lem2a  26101  pnt  26198  tglng  26340  axlowdimlem6  26741  axlowdimlem16  26751  axlowdimlem17  26752  axlowdim  26755  axeuclidlem  26756  axcontlem2  26759  axcontlem7  26764  axcontlem8  26765  nbusgrvtxm1uvtx  27195  wlk1walk  27428  pthdivtx  27518  pthdadjvtx  27519  crctcshwlkn0lem2  27597  crctcshwlkn0lem4  27599  clwwisshclwws  27800  fusgreg2wsp  28121  nvvcop  28377  nvex  28394  phnv  28597  sheli  28997  cheli  29015  hhssabloilem  29044  choc1  29110  shintcli  29112  chintcli  29114  shsleji  29153  pjini  29482  mayete3i  29511  dmadjop  29671  nlelshi  29843  cnlnadjeui  29860  cnlnssadj  29863  bdopadj  29865  pjimai  29959  stcl  29999  atelch  30127  fcnvgreu  30436  f1od2  30483  fcobijfs  30485  uzssico  30533  iundisj2fi  30546  nnindf  30561  eliccioo  30633  gsummptres  30737  cyc3genpm  30844  elrspunidl  31014  zarcls  31227  ordtrestNEW  31274  xrge0iifcnv  31286  xrge0iifcv  31287  xrge0iifiso  31288  xrge0iifhom  31290  qqhcn  31342  esumval  31415  gsumesum  31428  esumlub  31429  esumcst  31432  esumfsup  31439  issgon  31492  elrnsiga  31495  imambfm  31630  br2base  31637  sxbrsigalem0  31639  dya2iocucvr  31652  sxbrsigalem2  31654  sxbrsigalem5  31656  sxbrsiga  31658  omssubadd  31668  sitmcl  31719  oddpwdc  31722  eulerpartlemelr  31725  eulerpartlemgvv  31744  eulerpartlemgh  31746  eulerpartlemgs2  31748  eulerpartlemn  31749  sseqf  31760  ballotlem2  31856  ballotlemfp1  31859  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemfmpn  31862  ballotlemsup  31872  ballotlemfrceq  31896  signswch  31941  rpsqrtcn  31974  prodfzo03  31984  itgexpif  31987  bnj1533  32234  bnj1137  32377  bnj1286  32401  bnj1408  32418  bnj1417  32423  subfacp1lem5  32541  cvmsi  32622  gonar  32752  goalr  32754  mpst123  32897  mpstrcl  32898  msrrcl  32900  elmsta  32905  msubvrs  32917  elmpps  32930  elmthm  32933  bcprod  33080  dfon2lem4  33141  pprodss4v  33455  ivthALT  33793  neibastop2lem  33818  nnssi2  33913  nnssi3  33914  bj-sngltagi  34415  bj-elid5  34581  bj-fvmptunsn1  34669  bj-smgrpssmgmel  34681  bj-mndsssmgrpel  34683  bj-cmnssmndel  34685  bj-grpssmndel  34687  bj-ablssgrpel  34689  bj-ablsscmnel  34691  bj-vecssmodel  34694  bj-rveccvec  34716  bj-rvecabl  34718  taupilemrplb  34731  icorempo  34765  elxp8  34785  sin2h  35044  cos2h  35045  tan2h  35046  poimirlem14  35068  poimirlem26  35080  poimirlem27  35081  poimirlem31  35085  poimirlem32  35086  mblfinlem1  35091  cnambfre  35102  dvtan  35104  itg2addnc  35108  itg2gt0cn  35109  ftc1cnnc  35126  ftc2nc  35136  dvasin  35138  dvacos  35139  cover2  35149  sstotbnd2  35209  heibor1lem  35244  heiborlem10  35255  opidonOLD  35287  exidcl  35311  rngosn3  35359  flddivrng  35434  toycom  36266  osumcllem7N  37255  pexmidlem4N  37266  diaintclN  38351  dibintclN  38460  mapd1o  38941  hdmapevec  39128  prjspvs  39599  prjspeclsp  39601  0prjspnrel  39608  elrfi  39630  elrfirn  39631  elrfirn2  39632  mrefg3  39644  diophin  39708  diophun  39709  eq0rabdioph  39712  eqrabdioph  39713  pellex  39771  rmxycomplete  39853  jm2.23  39932  aomclem2  39994  fglmod  40012  lsmfgcl  40013  lmhmfgima  40023  lmhmfgsplit  40025  isnumbasabl  40045  dgrsub2  40074  itgocn  40103  areaquad  40161  elmapintrab  40271  corcltrcl  40435  k0004val0  40852  elscottab  40947  radcnvrat  41013  uzmptshftfval  41045  binomcxplemdvsum  41054  binomcxplemnotnn0  41055  onfrALTlem2  41247  onfrALTlem2VD  41590  uzwo4  41682  mptssid  41872  uzublem  42062  eliccelioc  42153  elicores  42165  sqrlearg  42185  fsumiunss  42212  limcdm0  42255  sumnnodd  42267  fnlimfvre  42311  limsupubuzlem  42349  limsupmnflem  42357  limsupre3uzlem  42372  climuzlem  42380  cncfshift  42511  cncfperiod  42516  icccncfext  42524  dvnprodlem1  42583  dvnprodlem2  42584  itgsin0pilem1  42587  itgsinexplem1  42591  itgsinexp  42592  ditgeqiooicc  42597  itgsubsticclem  42612  itgioocnicc  42614  itgsbtaddcnst  42619  stoweidlem34  42671  stoweidlem41  42678  stoweidlem51  42688  wallispilem2  42703  stirlinglem11  42721  dirkercncflem2  42741  fourierdlem5  42749  fourierdlem9  42753  fourierdlem17  42761  fourierdlem18  42762  fourierdlem20  42764  fourierdlem39  42783  fourierdlem48  42791  fourierdlem49  42792  fourierdlem62  42805  fourierdlem66  42809  fourierdlem68  42811  fourierdlem72  42815  fourierdlem73  42816  fourierdlem81  42824  fourierdlem83  42826  fourierdlem85  42828  fourierdlem87  42830  fourierdlem88  42831  fourierdlem92  42835  fourierdlem95  42838  fourierdlem103  42846  fourierdlem104  42847  fourierdlem112  42855  sqwvfoura  42865  sqwvfourb  42866  fouriersw  42868  etransclem24  42895  etransclem35  42906  etransclem37  42908  salexct  42969  salgencntex  42978  sge0resplit  43040  sge0split  43043  meaiuninclem  43114  caratheodorylem1  43160  volicorescl  43187  hoidmv1lelem3  43227  opnvonmbllem2  43267  ovolval2  43278  ovolval3  43281  ovolval4lem1  43283  ovolval4lem2  43284  pimiooltgt  43341  sssmf  43367  smfaddlem1  43391  smflimlem2  43400  smfrec  43416  smfdiv  43424  smfsuplem1  43437  smfsuplem3  43439  spr0el  43994  bgoldbtbndlem2  44319  bgoldbtbndlem3  44320  bgoldbtbnd  44322  fldhmsubc  44703  fldhmsubcALTV  44721
  Copyright terms: Public domain W3C validator