Theorem sseli 3945

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ss 3934

This theorem is referenced by:  sselii  3946  sselid  3947  elun1  4148  elun2  4149  elopabr  5524  elopabran  5525  elopaelxp  5731  copsex2ga  5773  2elresin  6642  nfvres  6902  fvco4i  6965  mptrcl  6980  fvmptss  6983  fvmptex  6985  fvmptnf  6993  elfvmptrab1w  6998  elfvmptrab1  6999  fvopab4ndm  7001  fvimacnvi  7027  elpreima  7033  iinpreima  7044  ofrfvalg  7664  ofval  7667  off  7674  nnon  7851  finds  7875  finds2  7877  eqopi  8007  op1steq  8015  dfoprab4  8037  bropopvvv  8072  bropfvvvv  8074  reldmtpos  8216  smores2  8326  frsuc  8408  unifpw  9313  cantnfp1lem1  9638  cantnfp1lem3  9640  r1fin  9733  r1tr  9736  r1ordg  9738  r1ord3g  9739  r1val1  9746  tz9.12lem3  9749  tcrank  9844  cplem1  9849  hta  9857  tskwe  9910  cardprclem  9939  alephfplem3  10066  dfac12r  10107  ackbij1lem16  10194  ackbij2  10202  fin23lem28  10300  fin23lem30  10302  fin23lem31  10303  fin1a2lem6  10365  hsmexlem4  10389  hsmexlem5  10390  hsmexlem6  10391  axdc2lem  10408  axdc3lem2  10411  axcclem  10417  brdom5  10489  brdom4  10490  r1tskina  10742  gruina  10778  grur1a  10779  pinn  10838  0nnq  10884  elpqn  10885  recn  11165  rexr  11227  ltord1  11711  leord1  11712  eqord1  11713  nnre  12200  nncn  12201  nnind  12211  nnnn0  12456  nn0re  12458  nn0cn  12459  nn0xnn0  12526  nnzOLD  12560  nn0z  12561  uzuzle35  12853  nnq  12928  qcn  12929  rpre  12967  eliccxr  13403  difreicc  13452  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  fzval2  13478  fzelp1  13544  4fvwrd4  13616  elfzo1  13680  ico01fl0  13788  expcllem  14044  expcl2lem  14045  m1expcl2  14057  bcm1k  14287  bcpasc  14293  hashbclem  14424  wrdv  14501  pfxfv0  14664  pfxfvlsw  14667  cshimadifsn  14802  swrds2m  14914  01sqrexlem5  15219  cau3lem  15328  caubnd  15332  climconst2  15521  o1of2  15586  o1rlimmul  15592  caurcvg  15650  caucvg  15652  binomlem  15802  incexclem  15809  divcnvshft  15828  zprod  15910  fprodge1  15968  risefaccllem  15986  fallfaccllem  15987  bpolydiflem  16027  bpoly4  16032  dvdsflip  16294  divalglem8  16377  sadadd  16444  smumul  16470  isprm3  16660  phimullem  16756  prmdiveq  16763  unbenlem  16886  vdwnnlem1  16973  vdwnnlem3  16975  ramtcl2  16989  prmgaplem4  17032  cshwshashlem1  17073  structcnvcnv  17130  fvsetsid  17145  imasdsval2  17486  mreunirn  17569  mrcfval  17576  mrisval  17598  coapm  18040  tsrss  18555  submnd0  18697  smndex1id  18845  nmzsubg  19104  nmznsg  19107  cntzmhm  19280  symgtrinv  19409  pmtrdifellem4  19416  psgnpmtr  19447  efginvrel2  19664  efginvrel1  19665  efgsp1  19674  efgsres  19675  efgsfo  19676  frgpinv  19701  frgpupf  19710  frgpup1  19712  subcmn  19774  torsubg  19791  dprd2dlem1  19980  dpjidcl  19997  ablfaclem3  20026  nzrring  20432  lringnzr  20457  fldhmsubc  20701  acsfn1p  20715  lssacs  20880  cnsubdrglem  21342  rege0subm  21347  rge0srg  21362  zringunit  21383  znrrg  21482  psgnghm  21496  zrhpsgnevpm  21507  evpmodpmf1o  21512  pmtrodpm  21513  phlssphl  21575  frlmsslsp  21712  islinds4  21751  lmimlbs  21752  lbslcic  21757  psrbaglefi  21842  psrbagconf1o  21845  mplsubglem  21915  mplneg  21926  ressmpladd  21943  ressmplmul  21944  ressmplvsca  21945  mplmonmul  21950  psdmul  22060  ply1bascl  22095  mdetralt  22502  mdetunilem7  22512  chfacfpmmulgsum2  22759  tgval2  22850  ordtbas  23086  ordtrestixx  23116  hauslly  23386  kgentop  23436  ptbasin  23471  filunirn  23776  uzrest  23791  elflim  23865  flffval  23883  fclsval  23902  isfcls  23903  fcfval  23927  ustn0  24115  fmucndlem  24185  xmetunirn  24232  mopnval  24333  setsmstopn  24373  tmsval  24376  tngtopn  24545  qtopbaslem  24653  xrtgioo  24702  reperflem  24714  icccmplem1  24718  icopnfhmeo  24848  icccvx  24855  bndth  24864  reparphtiOLD  24904  pcoval1  24920  pcoval2  24923  pcoass  24931  pcorevlem  24933  pcorev2  24935  pi1xfrcnv  24964  csscld  25156  cfilfval  25171  caufval  25182  bcthlem1  25231  ivthlem1  25359  ivthlem3  25361  ovolicc2lem3  25427  ovolicc2lem4  25428  vitalilem1  25516  mbflimsup  25574  i1fd  25589  i1f0  25595  i1f1  25598  itg1addlem4  25607  itg1addlem5  25608  iblmbf  25675  ellimc2  25785  limcres  25794  limcun  25803  dvbsss  25810  perfdvf  25811  dvres2lem  25818  dvaddbr  25847  rolle  25901  cmvth  25902  cmvthOLD  25903  dvlip  25905  dvlipcn  25906  dvle  25919  lhop1lem  25925  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc2  25958  itgparts  25961  itgsubstlem  25962  itgsubst  25963  deg1mul3  26028  coeval  26135  coeeu  26137  dgrval  26140  coef3  26144  coemulc  26167  dgrsub  26185  coecj  26191  coecjOLD  26193  dvply2  26201  dvnply  26203  quotval  26207  fta1  26223  plyexmo  26228  aacjcl  26242  taylfval  26273  dvtaylp  26285  abelth  26358  pilem3  26370  cos0pilt1  26448  sinord  26450  recosf1o  26451  resinf1o  26452  tanord1  26453  eff1olem  26464  dvloglem  26564  dvlog  26567  dvlog2lem  26568  advlogexp  26571  logtayl  26576  logtayl2  26578  dvcncxp1  26659  dvcnsqrt  26660  cxpcn3lem  26664  cxpcn3  26665  sqrtcn  26667  loglesqrt  26678  1cubr  26759  acosrecl  26820  efrlim  26886  efrlimOLD  26887  jensen  26906  lgamgulmlem2  26947  lgamucov2  26956  basellem4  27001  musum  27108  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dchrinvcl  27171  dchrghm  27174  dchrinv  27179  dchrsum2  27186  dchrsum  27187  rpvmasumlem  27405  dchrisum0lem2a  27435  pnt  27532  oldf  27772  leftirr  27809  rightirr  27810  lrold  27815  newbdayim  27821  sltlpss  27826  addsproplem2  27884  sleadd1  27903  addsuniflem  27915  addsbdaylem  27930  addsbday  27931  negsproplem2  27942  negsid  27954  negsunif  27968  mulsrid  28023  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  precsexlem9  28124  precsexlem11  28126  onsno  28163  onscutlt  28172  onaddscl  28181  onmulscl  28182  n0sno  28223  nnsno  28224  nnn0s  28227  nnsgt0  28238  zno  28277  expscllem  28323  tglng  28480  axlowdimlem6  28881  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  axeuclidlem  28896  axcontlem2  28899  axcontlem7  28904  axcontlem8  28905  nbusgrvtxm1uvtx  29339  wlk1walk  29574  pthdivtx  29664  pthdadjvtx  29665  crctcshwlkn0lem2  29748  crctcshwlkn0lem4  29750  clwwisshclwws  29951  fusgreg2wsp  30272  nvvcop  30530  nvex  30547  phnv  30750  sheli  31150  cheli  31168  hhssabloilem  31197  choc1  31263  shintcli  31265  chintcli  31267  shsleji  31306  pjini  31635  mayete3i  31664  dmadjop  31824  nlelshi  31996  cnlnadjeui  32013  cnlnssadj  32016  bdopadj  32018  pjimai  32112  stcl  32152  atelch  32280  fcnvgreu  32604  f1od2  32651  fcobijfs  32653  uzssico  32714  iundisj2fi  32727  nnindf  32751  eliccioo  32858  gsummptres  32999  cyc3genpm  33116  elrspunidl  33406  zarcls  33871  ordtrestNEW  33918  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  qqhcn  33988  esumval  34043  gsumesum  34056  esumlub  34057  esumcst  34060  esumfsup  34067  issgon  34120  elrnsiga  34123  imambfm  34260  br2base  34267  sxbrsigalem0  34269  dya2iocucvr  34282  sxbrsigalem2  34284  sxbrsigalem5  34286  sxbrsiga  34288  omssubadd  34298  sitmcl  34349  oddpwdc  34352  eulerpartlemelr  34355  eulerpartlemgvv  34374  eulerpartlemgh  34376  eulerpartlemgs2  34378  eulerpartlemn  34379  sseqf  34390  ballotlem2  34487  ballotlemfp1  34490  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemfmpn  34493  ballotlemsup  34503  ballotlemfrceq  34527  signswch  34559  rpsqrtcn  34591  prodfzo03  34601  itgexpif  34604  bnj1533  34849  bnj1137  34992  bnj1286  35016  bnj1408  35033  bnj1417  35038  onvf1odlem4  35100  subfacp1lem5  35178  cvmsi  35259  gonar  35389  goalr  35391  mpst123  35534  mpstrcl  35535  msrrcl  35537  elmsta  35542  msubvrs  35554  elmpps  35567  elmthm  35570  bcprod  35732  dfon2lem4  35781  pprodss4v  35879  ivthALT  36330  neibastop2lem  36355  nnssi2  36450  nnssi3  36451  bj-sngltagi  36977  bj-elid5  37164  bj-fvmptunsn1  37252  bj-smgrpssmgmel  37264  bj-mndsssmgrpel  37266  bj-cmnssmndel  37268  bj-grpssmndel  37270  bj-ablssgrpel  37272  bj-ablsscmnel  37274  bj-vecssmodel  37277  bj-flddrng  37284  bj-rveccvec  37300  bj-rvecabl  37302  taupilemrplb  37315  icorempo  37346  elxp8  37366  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem14  37635  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  poimirlem32  37653  mblfinlem1  37658  cnambfre  37669  dvtan  37671  itg2addnc  37675  itg2gt0cn  37676  ftc1cnnc  37693  ftc2nc  37703  dvasin  37705  dvacos  37706  cover2  37716  sstotbnd2  37775  heibor1lem  37810  heiborlem10  37821  opidonOLD  37853  exidcl  37877  rngosn3  37925  flddivrng  38000  toycom  38973  osumcllem7N  39963  pexmidlem4N  39974  diaintclN  41059  dibintclN  41168  mapd1o  41649  hdmapevec  41836  dvrelog2  42059  aks6d1c2lem4  42122  sticksstones1  42141  aks6d1c6lem5  42172  redvmptabs  42355  imacrhmcl  42509  prjspvs  42605  prjspeclsp  42607  0prjspnrel  42622  elrfi  42689  elrfirn  42690  elrfirn2  42691  mrefg3  42703  diophin  42767  diophun  42768  eq0rabdioph  42771  eqrabdioph  42772  pellex  42830  rmxycomplete  42913  jm2.23  42992  aomclem2  43051  fglmod  43069  lsmfgcl  43070  lmhmfgima  43080  lmhmfgsplit  43082  isnumbasabl  43102  dgrsub2  43131  itgocn  43160  areaquad  43212  cantnftermord  43316  omabs2  43328  nna1iscard  43541  elmapintrab  43572  corcltrcl  43735  k0004val0  44150  elscottab  44240  radcnvrat  44310  uzmptshftfval  44342  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  onfrALTlem2  44543  onfrALTlem2VD  44885  uzwo4  45054  mptssid  45242  uzublem  45433  eliccelioc  45526  elicores  45538  sqrlearg  45558  fsumiunss  45580  limcdm0  45623  sumnnodd  45635  fnlimfvre  45679  limsupubuzlem  45717  limsupmnflem  45725  limsupre3uzlem  45740  climuzlem  45748  liminflelimsuplem  45780  cncfshift  45879  cncfperiod  45884  icccncfext  45892  dvnprodlem1  45951  dvnprodlem2  45952  itgsin0pilem1  45955  itgsinexplem1  45959  itgsinexp  45960  ditgeqiooicc  45965  itgsubsticclem  45980  itgioocnicc  45982  itgsbtaddcnst  45987  stoweidlem34  46039  stoweidlem41  46046  stoweidlem51  46056  wallispilem2  46071  stirlinglem11  46089  dirkercncflem2  46109  fourierdlem5  46117  fourierdlem9  46121  fourierdlem17  46129  fourierdlem18  46130  fourierdlem20  46132  fourierdlem39  46151  fourierdlem48  46159  fourierdlem49  46160  fourierdlem62  46173  fourierdlem66  46177  fourierdlem68  46179  fourierdlem72  46183  fourierdlem73  46184  fourierdlem81  46192  fourierdlem83  46194  fourierdlem85  46196  fourierdlem87  46198  fourierdlem88  46199  fourierdlem92  46203  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  etransclem24  46263  etransclem35  46274  etransclem37  46276  salexct  46339  salgencntex  46348  sge0resplit  46411  sge0split  46414  meaiuninclem  46485  caratheodorylem1  46531  volicorescl  46558  hoidmv1lelem3  46598  opnvonmbllem2  46638  ovolval2  46649  ovolval3  46652  ovolval4lem1  46654  ovolval4lem2  46655  pimiooltgt  46715  sssmf  46743  smfaddlem1  46768  smflimlem2  46777  smfrec  46794  smfdiv  46802  smfsuplem1  46816  smfsuplem3  46818  et-ltneverrefl  46876  natglobalincr  46882  fcores  47072  rehalfge1  47340  spr0el  47487  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  upgrimpthslem2  47912  stgredgiun  47961  isubgr3stgrlem7  47975  fldhmsubcALTV  48325  fvconst0ci  48883  fvconstdomi  48884  idfullsubc  49154  fulloppf  49156  fthoppf  49157  initopropdlemlem  49232