Theorem sseli 3979

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 3976	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sselii  3980  sselid  3981  elun1  4177  elun2  4178  elopabr  5562  elopabran  5563  elopaelxp  5766  copsex2ga  5808  2elresin  6672  nfvres  6933  fvco4i  6993  mptrcl  7008  fvmptss  7011  fvmptex  7013  fvmptnf  7021  elfvmptrab1w  7025  elfvmptrab1  7026  fvopab4ndm  7028  fvimacnvi  7054  elpreima  7060  iinpreima  7071  ofrfvalg  7678  ofval  7681  off  7688  nnon  7861  finds  7889  finds2  7891  eqopi  8011  op1steq  8019  dfoprab4  8041  bropopvvv  8076  bropfvvvv  8078  reldmtpos  8219  wfrlem10OLD  8318  smores2  8354  frsuc  8437  nnfiOLD  9232  unifpw  9355  cantnfp1lem1  9673  cantnfp1lem3  9675  r1fin  9768  r1tr  9771  r1ordg  9773  r1ord3g  9774  r1val1  9781  tz9.12lem3  9784  tcrank  9879  cplem1  9884  hta  9892  tskwe  9945  cardprclem  9974  alephfplem3  10101  dfac12r  10141  ackbij1lem16  10230  ackbij2  10238  fin23lem28  10335  fin23lem30  10337  fin23lem31  10338  fin1a2lem6  10400  hsmexlem4  10424  hsmexlem5  10425  hsmexlem6  10426  axdc2lem  10443  axdc3lem2  10446  axcclem  10452  brdom5  10524  brdom4  10525  r1tskina  10777  gruina  10813  grur1a  10814  pinn  10873  0nnq  10919  elpqn  10920  recn  11200  rexr  11260  ltord1  11740  leord1  11741  eqord1  11742  nnre  12219  nncn  12220  nnind  12230  nnnn0  12479  nn0re  12481  nn0cn  12482  nn0xnn0  12548  nnzOLD  12582  nn0z  12583  nnq  12946  qcn  12947  rpre  12982  eliccxr  13412  difreicc  13461  iccshftri  13464  iccshftli  13466  iccdili  13468  icccntri  13470  fzval2  13487  fzelp1  13553  4fvwrd4  13621  elfzo1  13682  ico01fl0  13784  expcllem  14038  expcl2lem  14039  m1expcl2  14051  bcm1k  14275  bcpasc  14281  hashbclem  14411  wrdv  14479  pfxfv0  14642  pfxfvlsw  14645  cshimadifsn  14780  swrds2m  14892  01sqrexlem5  15193  cau3lem  15301  caubnd  15305  climconst2  15492  o1of2  15557  o1rlimmul  15563  caurcvg  15623  caucvg  15625  binomlem  15775  incexclem  15782  divcnvshft  15801  zprod  15881  fprodge1  15939  risefaccllem  15957  fallfaccllem  15958  bpolydiflem  15998  bpoly4  16003  dvdsflip  16260  divalglem8  16343  sadadd  16408  smumul  16434  isprm3  16620  phimullem  16712  prmdiveq  16719  unbenlem  16841  vdwnnlem1  16928  vdwnnlem3  16930  ramtcl2  16944  prmgaplem4  16987  cshwshashlem1  17029  structcnvcnv  17086  fvsetsid  17101  imasdsval2  17462  mreunirn  17545  mrcfval  17552  mrisval  17574  coapm  18021  tsrss  18542  submnd0  18654  smndex1id  18792  nmzsubg  19045  nmznsg  19048  cntzmhm  19205  symgtrinv  19340  pmtrdifellem4  19347  psgnpmtr  19378  efginvrel2  19595  efginvrel1  19596  efgsp1  19605  efgsres  19606  efgsfo  19607  frgpinv  19632  frgpupf  19641  frgpup1  19643  subcmn  19705  torsubg  19722  dprd2dlem1  19911  dpjidcl  19928  ablfaclem3  19957  nzrring  20295  lringnzr  20311  acsfn1p  20415  lssacs  20578  cnsubdrglem  20996  rege0subm  21001  rge0srg  21016  zringunit  21036  znrrg  21121  psgnghm  21133  zrhpsgnevpm  21144  evpmodpmf1o  21149  pmtrodpm  21150  phlssphl  21212  frlmsslsp  21351  islinds4  21390  lmimlbs  21391  lbslcic  21396  psrbaglefi  21485  psrbaglefiOLD  21486  psrbagconf1o  21489  mplsubglem  21558  mplneg  21569  ressmpladd  21584  ressmplmul  21585  ressmplvsca  21586  mplmonmul  21591  ply1bascl  21727  mdetralt  22110  mdetunilem7  22120  chfacfpmmulgsum2  22367  tgval2  22459  ordtbas  22696  ordtrestixx  22726  hauslly  22996  kgentop  23046  ptbasin  23081  filunirn  23386  uzrest  23401  elflim  23475  flffval  23493  fclsval  23512  isfcls  23513  fcfval  23537  ustn0  23725  fmucndlem  23796  xmetunirn  23843  mopnval  23944  setsmstopn  23986  tmsval  23989  tngtopn  24167  qtopbaslem  24275  xrtgioo  24322  reperflem  24334  icccmplem1  24338  icopnfhmeo  24459  icccvx  24466  bndth  24474  reparphti  24513  pcoval1  24529  pcoval2  24532  pcoass  24540  pcorevlem  24542  pcorev2  24544  pi1xfrcnv  24573  csscld  24766  cfilfval  24781  caufval  24792  bcthlem1  24841  ivthlem1  24968  ivthlem3  24970  ovolicc2lem3  25036  ovolicc2lem4  25037  vitalilem1  25125  mbflimsup  25183  i1fd  25198  i1f0  25204  i1f1  25207  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  iblmbf  25285  ellimc2  25394  limcres  25403  limcun  25412  dvbsss  25419  perfdvf  25420  dvres2lem  25427  dvaddbr  25455  rolle  25507  cmvth  25508  dvlip  25510  dvlipcn  25511  dvle  25524  lhop1lem  25530  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  dvfsumlem2  25544  ftc2  25561  itgparts  25564  itgsubstlem  25565  itgsubst  25566  deg1mul3  25633  coeval  25737  coeeu  25739  dgrval  25742  coef3  25746  coemulc  25769  dgrsub  25786  coecj  25792  dvply2  25799  dvnply  25801  quotval  25805  fta1  25821  plyexmo  25826  aacjcl  25840  taylfval  25871  dvtaylp  25882  abelth  25953  pilem3  25965  cos0pilt1  26041  sinord  26043  recosf1o  26044  resinf1o  26045  tanord1  26046  eff1olem  26057  dvloglem  26156  dvlog  26159  dvlog2lem  26160  advlogexp  26163  logtayl  26168  logtayl2  26170  dvcncxp1  26251  dvcnsqrt  26252  cxpcn3lem  26255  cxpcn3  26256  sqrtcn  26258  loglesqrt  26266  1cubr  26347  acosrecl  26408  efrlim  26474  jensen  26493  lgamgulmlem2  26534  lgamucov2  26543  basellem4  26588  musum  26695  dchrinvcl  26756  dchrghm  26759  dchrinv  26764  dchrsum2  26771  dchrsum  26772  rpvmasumlem  26990  dchrisum0lem2a  27020  pnt  27117  oldf  27352  leftirr  27385  rightirr  27386  lrold  27391  sltlpss  27401  addsproplem2  27454  sleadd1  27472  addsuniflem  27484  negsproplem2  27503  negsid  27515  negsunif  27529  mulsrid  27569  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  precsexlem9  27661  precsexlem11  27663  tglng  27797  axlowdimlem6  28205  axlowdimlem16  28215  axlowdimlem17  28216  axlowdim  28219  axeuclidlem  28220  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  nbusgrvtxm1uvtx  28662  wlk1walk  28896  pthdivtx  28986  pthdadjvtx  28987  crctcshwlkn0lem2  29065  crctcshwlkn0lem4  29067  clwwisshclwws  29268  fusgreg2wsp  29589  nvvcop  29847  nvex  29864  phnv  30067  sheli  30467  cheli  30485  hhssabloilem  30514  choc1  30580  shintcli  30582  chintcli  30584  shsleji  30623  pjini  30952  mayete3i  30981  dmadjop  31141  nlelshi  31313  cnlnadjeui  31330  cnlnssadj  31333  bdopadj  31335  pjimai  31429  stcl  31469  atelch  31597  fcnvgreu  31898  f1od2  31946  fcobijfs  31948  uzssico  31995  iundisj2fi  32008  nnindf  32025  eliccioo  32097  gsummptres  32204  cyc3genpm  32311  elrspunidl  32546  zarcls  32854  ordtrestNEW  32901  xrge0iifcnv  32913  xrge0iifcv  32914  xrge0iifiso  32915  xrge0iifhom  32917  qqhcn  32971  esumval  33044  gsumesum  33057  esumlub  33058  esumcst  33061  esumfsup  33068  issgon  33121  elrnsiga  33124  imambfm  33261  br2base  33268  sxbrsigalem0  33270  dya2iocucvr  33283  sxbrsigalem2  33285  sxbrsigalem5  33287  sxbrsiga  33289  omssubadd  33299  sitmcl  33350  oddpwdc  33353  eulerpartlemelr  33356  eulerpartlemgvv  33375  eulerpartlemgh  33377  eulerpartlemgs2  33379  eulerpartlemn  33380  sseqf  33391  ballotlem2  33487  ballotlemfp1  33490  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemfmpn  33493  ballotlemsup  33503  ballotlemfrceq  33527  signswch  33572  rpsqrtcn  33605  prodfzo03  33615  itgexpif  33618  bnj1533  33863  bnj1137  34006  bnj1286  34030  bnj1408  34047  bnj1417  34052  subfacp1lem5  34175  cvmsi  34256  gonar  34386  goalr  34388  mpst123  34531  mpstrcl  34532  msrrcl  34534  elmsta  34539  msubvrs  34551  elmpps  34564  elmthm  34567  bcprod  34708  dfon2lem4  34758  pprodss4v  34856  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  ivthALT  35220  neibastop2lem  35245  nnssi2  35340  nnssi3  35341  bj-sngltagi  35863  bj-elid5  36050  bj-fvmptunsn1  36138  bj-smgrpssmgmel  36150  bj-mndsssmgrpel  36152  bj-cmnssmndel  36154  bj-grpssmndel  36156  bj-ablssgrpel  36158  bj-ablsscmnel  36160  bj-vecssmodel  36163  bj-flddrng  36170  bj-rveccvec  36186  bj-rvecabl  36188  taupilemrplb  36201  icorempo  36232  elxp8  36252  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem14  36502  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  mblfinlem1  36525  cnambfre  36536  dvtan  36538  itg2addnc  36542  itg2gt0cn  36543  ftc1cnnc  36560  ftc2nc  36570  dvasin  36572  dvacos  36573  cover2  36583  sstotbnd2  36642  heibor1lem  36677  heiborlem10  36688  opidonOLD  36720  exidcl  36744  rngosn3  36792  flddivrng  36867  toycom  37843  osumcllem7N  38833  pexmidlem4N  38844  diaintclN  39929  dibintclN  40038  mapd1o  40519  hdmapevec  40706  dvrelog2  40929  sticksstones1  40962  imacrhmcl  41089  prjspvs  41352  prjspeclsp  41354  0prjspnrel  41369  elrfi  41432  elrfirn  41433  elrfirn2  41434  mrefg3  41446  diophin  41510  diophun  41511  eq0rabdioph  41514  eqrabdioph  41515  pellex  41573  rmxycomplete  41656  jm2.23  41735  aomclem2  41797  fglmod  41815  lsmfgcl  41816  lmhmfgima  41826  lmhmfgsplit  41828  isnumbasabl  41848  dgrsub2  41877  itgocn  41906  areaquad  41965  cantnftermord  42070  omabs2  42082  nna1iscard  42296  elmapintrab  42327  corcltrcl  42490  k0004val0  42905  elscottab  43003  radcnvrat  43073  uzmptshftfval  43105  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  onfrALTlem2  43307  onfrALTlem2VD  43650  uzwo4  43740  mptssid  43944  uzublem  44140  eliccelioc  44234  elicores  44246  sqrlearg  44266  fsumiunss  44291  limcdm0  44334  sumnnodd  44346  fnlimfvre  44390  limsupubuzlem  44428  limsupmnflem  44436  limsupre3uzlem  44451  climuzlem  44459  cncfshift  44590  cncfperiod  44595  icccncfext  44603  dvnprodlem1  44662  dvnprodlem2  44663  itgsin0pilem1  44666  itgsinexplem1  44670  itgsinexp  44671  ditgeqiooicc  44676  itgsubsticclem  44691  itgioocnicc  44693  itgsbtaddcnst  44698  stoweidlem34  44750  stoweidlem41  44757  stoweidlem51  44767  wallispilem2  44782  stirlinglem11  44800  dirkercncflem2  44820  fourierdlem5  44828  fourierdlem9  44832  fourierdlem17  44840  fourierdlem18  44841  fourierdlem20  44843  fourierdlem39  44862  fourierdlem48  44870  fourierdlem49  44871  fourierdlem62  44884  fourierdlem66  44888  fourierdlem68  44890  fourierdlem72  44894  fourierdlem73  44895  fourierdlem81  44903  fourierdlem83  44905  fourierdlem85  44907  fourierdlem87  44909  fourierdlem88  44910  fourierdlem92  44914  fourierdlem95  44917  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  sqwvfoura  44944  sqwvfourb  44945  fouriersw  44947  etransclem24  44974  etransclem35  44985  etransclem37  44987  salexct  45050  salgencntex  45059  sge0resplit  45122  sge0split  45125  meaiuninclem  45196  caratheodorylem1  45242  volicorescl  45269  hoidmv1lelem3  45309  opnvonmbllem2  45349  ovolval2  45360  ovolval3  45363  ovolval4lem1  45365  ovolval4lem2  45366  pimiooltgt  45426  sssmf  45454  smfaddlem1  45479  smflimlem2  45488  smfrec  45505  smfdiv  45513  smfsuplem1  45527  smfsuplem3  45529  et-ltneverrefl  45587  natglobalincr  45591  fcores  45777  spr0el  46150  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  fldhmsubc  46982  fldhmsubcALTV  47000  fvconst0ci  47525  fvconstdomi  47526