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

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssel 3909	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-ss 3900

This theorem is referenced by:  sselii  3912  sselid  3913  elun1  4111  elun2  4112  elopabr  5502  elopabran  5503  elopaelxp  5708  copsex2ga  5750  2elresin  6606  nfvres  6865  fvco4i  6929  mptrcl  6945  fvmptss  6948  fvmptex  6950  fvmptnf  6958  elfvmptrab1w  6963  elfvmptrab1  6964  fvopab4ndm  6966  fvimacnvi  6993  elpreima  6999  iinpreima  7010  ofrfvalg  7628  ofval  7631  off  7638  nnon  7812  finds  7836  finds2  7838  eqopi  7967  op1steq  7975  dfoprab4  7997  bropopvvv  8029  bropfvvvv  8031  reldmtpos  8174  smores2  8284  frsuc  8366  unifpw  9255  cantnfp1lem1  9590  cantnfp1lem3  9592  r1fin  9688  r1tr  9691  r1ordg  9693  r1ord3g  9694  r1val1  9701  tz9.12lem3  9704  tcrank  9799  cplem1  9804  hta  9812  tskwe  9865  cardprclem  9894  alephfplem3  10019  dfac12r  10060  ackbij1lem16  10147  ackbij2  10155  fin23lem28  10253  fin23lem30  10255  fin23lem31  10256  fin1a2lem6  10318  hsmexlem4  10342  hsmexlem5  10343  hsmexlem6  10344  axdc2lem  10361  axdc3lem2  10364  axcclem  10370  brdom5  10442  brdom4  10443  r1tskina  10696  gruina  10732  grur1a  10733  pinn  10792  0nnq  10838  elpqn  10839  recn  11119  rexr  11182  ltord1  11667  leord1  11668  eqord1  11669  nnre  12172  nncn  12173  nnind  12183  nnnn0  12435  nn0re  12437  nn0cn  12438  nn0xnn0  12505  nn0z  12539  uzuzle35  12828  nnq  12903  qcn  12904  rpre  12942  eliccxr  13379  difreicc  13428  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  fzval2  13455  fzelp1  13521  4fvwrd4  13593  elfzo1  13658  ico01fl0  13769  expcllem  14025  expcl2lem  14026  m1expcl2  14038  bcm1k  14268  bcpasc  14274  hashbclem  14405  wrdv  14482  pfxfv0  14645  pfxfvlsw  14648  cshimadifsn  14782  swrds2m  14894  01sqrexlem5  15199  cau3lem  15308  caubnd  15312  climconst2  15501  o1of2  15566  o1rlimmul  15572  caurcvg  15630  caucvg  15632  binomlem  15785  incexclem  15792  divcnvshft  15811  zprod  15893  fprodge1  15951  risefaccllem  15969  fallfaccllem  15970  bpolydiflem  16010  bpoly4  16015  dvdsflip  16277  divalglem8  16360  sadadd  16427  smumul  16453  isprm3  16643  phimullem  16740  prmdiveq  16747  unbenlem  16870  vdwnnlem1  16957  vdwnnlem3  16959  ramtcl2  16973  prmgaplem4  17016  cshwshashlem1  17057  structcnvcnv  17114  fvsetsid  17129  imasdsval2  17471  mreunirn  17554  mrcfval  17565  mrisval  17587  coapm  18029  tsrss  18546  chnccat  18583  ex-chn1  18594  submnd0  18722  smndex1id  18873  nmzsubg  19131  nmznsg  19134  cntzmhm  19307  symgtrinv  19438  pmtrdifellem4  19445  psgnpmtr  19476  efginvrel2  19693  efginvrel1  19694  efgsp1  19703  efgsres  19704  efgsfo  19705  frgpinv  19730  frgpupf  19739  frgpup1  19741  subcmn  19803  torsubg  19820  dprd2dlem1  20009  dpjidcl  20026  ablfaclem3  20055  nzrring  20488  lringnzr  20513  fldhmsubc  20757  acsfn1p  20771  lssacs  20957  cnsubdrglem  21393  rege0subm  21398  rge0srg  21413  zringunit  21441  znrrg  21540  psgnghm  21555  zrhpsgnevpm  21566  evpmodpmf1o  21571  pmtrodpm  21572  phlssphl  21634  frlmsslsp  21771  islinds4  21810  lmimlbs  21811  lbslcic  21816  psrbaglefi  21901  psrbagconf1o  21904  mplsubglem  21973  mplneg  21984  ressmpladd  22004  ressmplmul  22005  ressmplvsca  22006  mplmonmul  22012  psdmul  22154  ply1bascl  22188  mdetralt  22591  mdetunilem7  22601  chfacfpmmulgsum2  22848  tgval2  22939  ordtbas  23175  ordtrestixx  23205  hauslly  23475  kgentop  23525  ptbasin  23560  filunirn  23865  uzrest  23880  elflim  23954  flffval  23972  fclsval  23991  isfcls  23992  fcfval  24016  ustn0  24204  fmucndlem  24273  xmetunirn  24320  mopnval  24421  setsmstopn  24461  tmsval  24464  tngtopn  24633  qtopbaslem  24741  xrtgioo  24790  reperflem  24802  icccmplem1  24806  icopnfhmeo  24928  icccvx  24935  bndth  24943  pcoval1  24998  pcoval2  25001  pcoass  25009  pcorevlem  25011  pcorev2  25013  pi1xfrcnv  25042  csscld  25234  cfilfval  25249  caufval  25260  bcthlem1  25309  ivthlem1  25436  ivthlem3  25438  ovolicc2lem3  25504  ovolicc2lem4  25505  vitalilem1  25593  mbflimsup  25651  i1fd  25666  i1f0  25672  i1f1  25675  itg1addlem4  25684  itg1addlem5  25685  iblmbf  25752  ellimc2  25862  limcres  25871  limcun  25880  dvbsss  25887  perfdvf  25888  dvres2lem  25895  dvaddbr  25923  rolle  25975  cmvth  25976  dvlip  25978  dvlipcn  25979  dvle  25992  lhop1lem  25998  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  dvfsumlem2  26012  ftc2  26029  itgparts  26032  itgsubstlem  26033  itgsubst  26034  deg1mul3  26099  coeval  26206  coeeu  26208  dgrval  26211  coef3  26215  coemulc  26238  dgrsub  26255  coecj  26261  coecjOLD  26263  dvply2  26270  dvnply  26272  quotval  26276  fta1  26292  plyexmo  26297  aacjcl  26311  taylfval  26342  dvtaylp  26353  abelth  26424  pilem3  26436  cos0pilt1  26514  sinord  26516  recosf1o  26517  resinf1o  26518  tanord1  26519  eff1olem  26530  dvloglem  26630  dvlog  26633  dvlog2lem  26634  advlogexp  26637  logtayl  26642  logtayl2  26644  dvcncxp1  26725  dvcnsqrt  26726  cxpcn3lem  26729  cxpcn3  26730  sqrtcn  26732  loglesqrt  26743  1cubr  26824  acosrecl  26885  efrlim  26951  jensen  26970  lgamgulmlem2  27011  lgamucov2  27020  basellem4  27065  musum  27172  mpodvdsmulf1o  27175  fsumdvdsmul  27176  dchrinvcl  27234  dchrghm  27237  dchrinv  27242  dchrsum2  27249  dchrsum  27250  rpvmasumlem  27468  dchrisum0lem2a  27498  pnt  27595  oldf  27847  madeno  27853  oldno  27854  newno  27855  oldmade  27878  leftold  27885  rightold  27886  leftno  27887  rightno  27888  addbdaylem  28027  addbday  28028  negsproplem2  28039  negsid  28051  negsunif  28065  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  precsexlem11  28227  onno  28265  oncutlt  28274  n0no  28333  nnno  28334  nnn0s  28337  nnsgt0  28349  zno  28392  expscllem  28440  tglng  28632  axlowdimlem6  29034  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  axeuclidlem  29049  axcontlem2  29052  axcontlem7  29057  axcontlem8  29058  nbusgrvtxm1uvtx  29492  wlk1walk  29725  pthdivtx  29813  pthdadjvtx  29814  crctcshwlkn0lem2  29897  crctcshwlkn0lem4  29899  clwwisshclwws  30103  fusgreg2wsp  30424  nvvcop  30683  nvex  30700  phnv  30903  sheli  31303  cheli  31321  hhssabloilem  31350  choc1  31416  shintcli  31418  chintcli  31420  shsleji  31459  pjini  31788  mayete3i  31817  dmadjop  31977  nlelshi  32149  cnlnadjeui  32166  cnlnssadj  32169  bdopadj  32171  pjimai  32265  stcl  32305  atelch  32433  fcnvgreu  32764  f1od2  32811  fcobijfs  32813  fcobijfs2  32814  uzssico  32876  iundisj2fi  32889  nnindf  32912  eliccioo  33009  gsummptres  33133  cyc3genpm  33233  elrspunidl  33511  0mplrim  33698  psrmonmul  33734  zarcls  34058  ordtrestNEW  34105  xrge0iifcnv  34117  xrge0iifcv  34118  xrge0iifiso  34119  xrge0iifhom  34121  qqhcn  34175  esumval  34230  gsumesum  34243  esumlub  34244  esumcst  34247  esumfsup  34254  issgon  34307  elrnsiga  34310  imambfm  34446  br2base  34453  sxbrsigalem0  34455  dya2iocucvr  34468  sxbrsigalem2  34470  sxbrsigalem5  34472  sxbrsiga  34474  omssubadd  34484  sitmcl  34535  oddpwdc  34538  eulerpartlemelr  34541  eulerpartlemgvv  34560  eulerpartlemgh  34562  eulerpartlemgs2  34564  eulerpartlemn  34565  sseqf  34576  ballotlem2  34673  ballotlemfp1  34676  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemfmpn  34679  ballotlemsup  34689  ballotlemfrceq  34713  signswch  34745  rpsqrtcn  34777  prodfzo03  34787  itgexpif  34790  bnj1533  35034  bnj1137  35177  bnj1286  35201  bnj1408  35218  bnj1417  35223  r1omhf  35287  onvf1odlem4  35334  subfacp1lem5  35412  cvmsi  35493  gonar  35623  goalr  35625  mpst123  35768  mpstrcl  35769  msrrcl  35771  elmsta  35776  msubvrs  35788  elmpps  35801  elmthm  35804  bcprod  35966  dfon2lem4  36012  pprodss4v  36110  ivthALT  36563  neibastop2lem  36588  nnssi2  36683  nnssi3  36684  ttcel2  36729  bj-sngltagi  37335  bj-elid5  37529  bj-fvmptunsn1  37617  bj-smgrpssmgmel  37629  bj-mndsssmgrpel  37631  bj-cmnssmndel  37633  bj-grpssmndel  37635  bj-ablssgrpel  37637  bj-ablsscmnel  37639  bj-vecssmodel  37642  bj-flddrng  37649  bj-rveccvec  37665  bj-rvecabl  37667  taupilemrplb  37680  icorempo  37713  elxp8  37733  sin2h  37977  cos2h  37978  tan2h  37979  poimirlem14  38001  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  mblfinlem1  38024  cnambfre  38035  dvtan  38037  itg2addnc  38041  itg2gt0cn  38042  ftc1cnnc  38059  ftc2nc  38069  dvasin  38071  dvacos  38072  cover2  38082  sstotbnd2  38141  heibor1lem  38176  heiborlem10  38187  opidonOLD  38219  exidcl  38243  rngosn3  38291  flddivrng  38366  toycom  39465  osumcllem7N  40454  pexmidlem4N  40465  diaintclN  41550  dibintclN  41659  mapd1o  42140  hdmapevec  42327  dvrelog2  42549  aks6d1c2lem4  42612  sticksstones1  42631  aks6d1c6lem5  42662  redvmptabs  42837  imacrhmcl  43004  prjspvs  43060  prjspeclsp  43062  0prjspnrel  43077  elrfi  43143  elrfirn  43144  elrfirn2  43145  mrefg3  43157  diophin  43221  diophun  43222  eq0rabdioph  43225  eqrabdioph  43226  pellex  43280  rmxycomplete  43362  jm2.23  43441  aomclem2  43500  fglmod  43518  lsmfgcl  43519  lmhmfgima  43529  lmhmfgsplit  43531  isnumbasabl  43551  dgrsub2  43580  itgocn  43609  areaquad  43661  cantnftermord  43765  omabs2  43777  nna1iscard  43989  elmapintrab  44020  corcltrcl  44183  k0004val0  44598  elscottab  44688  radcnvrat  44758  uzmptshftfval  44790  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  onfrALTlem2  44990  onfrALTlem2VD  45332  uzwo4  45501  mptssid  45685  uzublem  45873  eliccelioc  45966  elicores  45978  sqrlearg  45998  fsumiunss  46020  limcdm0  46063  sumnnodd  46075  fnlimfvre  46117  limsupubuzlem  46155  limsupmnflem  46163  limsupre3uzlem  46178  climuzlem  46186  liminflelimsuplem  46218  cncfshift  46317  cncfperiod  46322  icccncfext  46330  dvnprodlem1  46389  dvnprodlem2  46390  itgsin0pilem1  46393  itgsinexplem1  46397  itgsinexp  46398  ditgeqiooicc  46403  itgsubsticclem  46418  itgioocnicc  46420  itgsbtaddcnst  46425  stoweidlem34  46477  stoweidlem41  46484  stoweidlem51  46494  wallispilem2  46509  stirlinglem11  46527  dirkercncflem2  46547  fourierdlem5  46555  fourierdlem9  46559  fourierdlem17  46567  fourierdlem18  46568  fourierdlem20  46570  fourierdlem39  46589  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem66  46615  fourierdlem68  46617  fourierdlem72  46621  fourierdlem73  46622  fourierdlem81  46630  fourierdlem83  46632  fourierdlem85  46634  fourierdlem87  46636  fourierdlem88  46637  fourierdlem92  46641  fourierdlem95  46644  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  sqwvfoura  46671  sqwvfourb  46672  fouriersw  46674  etransclem24  46701  etransclem35  46712  etransclem37  46714  salexct  46777  salgencntex  46786  sge0resplit  46849  sge0split  46852  meaiuninclem  46923  caratheodorylem1  46969  volicorescl  46996  hoidmv1lelem3  47036  opnvonmbllem2  47076  ovolval2  47087  ovolval3  47090  ovolval4lem1  47092  ovolval4lem2  47093  sssmf  47181  smfaddlem1  47206  smflimlem2  47215  smfrec  47232  smfdiv  47240  smfsuplem1  47254  smfsuplem3  47256  et-ltneverrefl  47314  natglobalincr  47322  tannpoly  47353  fcores  47530  elfz2nn  47785  rehalfge1  47802  spr0el  47957  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  upgrimpthslem2  48399  stgredgiun  48449  isubgr3stgrlem7  48463  fldhmsubcALTV  48824  fvconst0ci  49381  fvconstdomi  49382  idfullsubc  49651  fulloppf  49653  fthoppf  49654  initopropdlemlem  49729