Theorem sseli 3929

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ss 3918

This theorem is referenced by:  sselii  3930  sselid  3931  elun1  4134  elun2  4135  elopabr  5508  elopabran  5509  elopaelxp  5714  copsex2ga  5756  2elresin  6613  nfvres  6872  fvco4i  6935  mptrcl  6950  fvmptss  6953  fvmptex  6955  fvmptnf  6963  elfvmptrab1w  6968  elfvmptrab1  6969  fvopab4ndm  6971  fvimacnvi  6997  elpreima  7003  iinpreima  7014  ofrfvalg  7630  ofval  7633  off  7640  nnon  7814  finds  7838  finds2  7840  eqopi  7969  op1steq  7977  dfoprab4  7999  bropopvvv  8032  bropfvvvv  8034  reldmtpos  8176  smores2  8286  frsuc  8368  unifpw  9255  cantnfp1lem1  9587  cantnfp1lem3  9589  r1fin  9685  r1tr  9688  r1ordg  9690  r1ord3g  9691  r1val1  9698  tz9.12lem3  9701  tcrank  9796  cplem1  9801  hta  9809  tskwe  9862  cardprclem  9891  alephfplem3  10016  dfac12r  10057  ackbij1lem16  10144  ackbij2  10152  fin23lem28  10250  fin23lem30  10252  fin23lem31  10253  fin1a2lem6  10315  hsmexlem4  10339  hsmexlem5  10340  hsmexlem6  10341  axdc2lem  10358  axdc3lem2  10361  axcclem  10367  brdom5  10439  brdom4  10440  r1tskina  10693  gruina  10729  grur1a  10730  pinn  10789  0nnq  10835  elpqn  10836  recn  11116  rexr  11178  ltord1  11663  leord1  11664  eqord1  11665  nnre  12152  nncn  12153  nnind  12163  nnnn0  12408  nn0re  12410  nn0cn  12411  nn0xnn0  12478  nn0z  12512  uzuzle35  12800  nnq  12875  qcn  12876  rpre  12914  eliccxr  13351  difreicc  13400  iccshftri  13403  iccshftli  13405  iccdili  13407  icccntri  13409  fzval2  13426  fzelp1  13492  4fvwrd4  13564  elfzo1  13628  ico01fl0  13739  expcllem  13995  expcl2lem  13996  m1expcl2  14008  bcm1k  14238  bcpasc  14244  hashbclem  14375  wrdv  14452  pfxfv0  14615  pfxfvlsw  14618  cshimadifsn  14752  swrds2m  14864  01sqrexlem5  15169  cau3lem  15278  caubnd  15282  climconst2  15471  o1of2  15536  o1rlimmul  15542  caurcvg  15600  caucvg  15602  binomlem  15752  incexclem  15759  divcnvshft  15778  zprod  15860  fprodge1  15918  risefaccllem  15936  fallfaccllem  15937  bpolydiflem  15977  bpoly4  15982  dvdsflip  16244  divalglem8  16327  sadadd  16394  smumul  16420  isprm3  16610  phimullem  16706  prmdiveq  16713  unbenlem  16836  vdwnnlem1  16923  vdwnnlem3  16925  ramtcl2  16939  prmgaplem4  16982  cshwshashlem1  17023  structcnvcnv  17080  fvsetsid  17095  imasdsval2  17437  mreunirn  17520  mrcfval  17531  mrisval  17553  coapm  17995  tsrss  18512  chnccat  18549  ex-chn1  18560  submnd0  18688  smndex1id  18836  nmzsubg  19094  nmznsg  19097  cntzmhm  19270  symgtrinv  19401  pmtrdifellem4  19408  psgnpmtr  19439  efginvrel2  19656  efginvrel1  19657  efgsp1  19666  efgsres  19667  efgsfo  19668  frgpinv  19693  frgpupf  19702  frgpup1  19704  subcmn  19766  torsubg  19783  dprd2dlem1  19972  dpjidcl  19989  ablfaclem3  20018  nzrring  20449  lringnzr  20474  fldhmsubc  20718  acsfn1p  20732  lssacs  20918  cnsubdrglem  21373  rege0subm  21378  rge0srg  21393  zringunit  21421  znrrg  21520  psgnghm  21535  zrhpsgnevpm  21546  evpmodpmf1o  21551  pmtrodpm  21552  phlssphl  21614  frlmsslsp  21751  islinds4  21790  lmimlbs  21791  lbslcic  21796  psrbaglefi  21882  psrbagconf1o  21885  mplsubglem  21954  mplneg  21965  ressmpladd  21984  ressmplmul  21985  ressmplvsca  21986  mplmonmul  21991  psdmul  22109  ply1bascl  22144  mdetralt  22552  mdetunilem7  22562  chfacfpmmulgsum2  22809  tgval2  22900  ordtbas  23136  ordtrestixx  23166  hauslly  23436  kgentop  23486  ptbasin  23521  filunirn  23826  uzrest  23841  elflim  23915  flffval  23933  fclsval  23952  isfcls  23953  fcfval  23977  ustn0  24165  fmucndlem  24234  xmetunirn  24281  mopnval  24382  setsmstopn  24422  tmsval  24425  tngtopn  24594  qtopbaslem  24702  xrtgioo  24751  reperflem  24763  icccmplem1  24767  icopnfhmeo  24897  icccvx  24904  bndth  24913  reparphtiOLD  24953  pcoval1  24969  pcoval2  24972  pcoass  24980  pcorevlem  24982  pcorev2  24984  pi1xfrcnv  25013  csscld  25205  cfilfval  25220  caufval  25231  bcthlem1  25280  ivthlem1  25408  ivthlem3  25410  ovolicc2lem3  25476  ovolicc2lem4  25477  vitalilem1  25565  mbflimsup  25623  i1fd  25638  i1f0  25644  i1f1  25647  itg1addlem4  25656  itg1addlem5  25657  iblmbf  25724  ellimc2  25834  limcres  25843  limcun  25852  dvbsss  25859  perfdvf  25860  dvres2lem  25867  dvaddbr  25896  rolle  25950  cmvth  25951  cmvthOLD  25952  dvlip  25954  dvlipcn  25955  dvle  25968  lhop1lem  25974  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc2  26007  itgparts  26010  itgsubstlem  26011  itgsubst  26012  deg1mul3  26077  coeval  26184  coeeu  26186  dgrval  26189  coef3  26193  coemulc  26216  dgrsub  26234  coecj  26240  coecjOLD  26242  dvply2  26250  dvnply  26252  quotval  26256  fta1  26272  plyexmo  26277  aacjcl  26291  taylfval  26322  dvtaylp  26334  abelth  26407  pilem3  26419  cos0pilt1  26497  sinord  26499  recosf1o  26500  resinf1o  26501  tanord1  26502  eff1olem  26513  dvloglem  26613  dvlog  26616  dvlog2lem  26617  advlogexp  26620  logtayl  26625  logtayl2  26627  dvcncxp1  26708  dvcnsqrt  26709  cxpcn3lem  26713  cxpcn3  26714  sqrtcn  26716  loglesqrt  26727  1cubr  26808  acosrecl  26869  efrlim  26935  efrlimOLD  26936  jensen  26955  lgamgulmlem2  26996  lgamucov2  27005  basellem4  27050  musum  27157  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dchrinvcl  27220  dchrghm  27223  dchrinv  27228  dchrsum2  27235  dchrsum  27236  rpvmasumlem  27454  dchrisum0lem2a  27484  pnt  27581  oldf  27833  madeno  27839  oldno  27840  newno  27841  oldmade  27864  leftold  27871  rightold  27872  leftno  27873  rightno  27874  addbdaylem  28013  addbday  28014  negsproplem2  28025  negsid  28037  negsunif  28051  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  precsexlem11  28213  onno  28251  oncutlt  28260  n0no  28319  nnno  28320  nnn0s  28323  nnsgt0  28335  zno  28378  expscllem  28426  tglng  28618  axlowdimlem6  29020  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  axeuclidlem  29035  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  nbusgrvtxm1uvtx  29478  wlk1walk  29712  pthdivtx  29800  pthdadjvtx  29801  crctcshwlkn0lem2  29884  crctcshwlkn0lem4  29886  clwwisshclwws  30090  fusgreg2wsp  30411  nvvcop  30669  nvex  30686  phnv  30889  sheli  31289  cheli  31307  hhssabloilem  31336  choc1  31402  shintcli  31404  chintcli  31406  shsleji  31445  pjini  31774  mayete3i  31803  dmadjop  31963  nlelshi  32135  cnlnadjeui  32152  cnlnssadj  32155  bdopadj  32157  pjimai  32251  stcl  32291  atelch  32419  fcnvgreu  32751  f1od2  32798  fcobijfs  32800  fcobijfs2  32801  uzssico  32864  iundisj2fi  32877  nnindf  32900  eliccioo  33012  gsummptres  33135  cyc3genpm  33234  elrspunidl  33509  zarcls  34031  ordtrestNEW  34078  xrge0iifcnv  34090  xrge0iifcv  34091  xrge0iifiso  34092  xrge0iifhom  34094  qqhcn  34148  esumval  34203  gsumesum  34216  esumlub  34217  esumcst  34220  esumfsup  34227  issgon  34280  elrnsiga  34283  imambfm  34419  br2base  34426  sxbrsigalem0  34428  dya2iocucvr  34441  sxbrsigalem2  34443  sxbrsigalem5  34445  sxbrsiga  34447  omssubadd  34457  sitmcl  34508  oddpwdc  34511  eulerpartlemelr  34514  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemgs2  34537  eulerpartlemn  34538  sseqf  34549  ballotlem2  34646  ballotlemfp1  34649  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemfmpn  34652  ballotlemsup  34662  ballotlemfrceq  34686  signswch  34718  rpsqrtcn  34750  prodfzo03  34760  itgexpif  34763  bnj1533  35008  bnj1137  35151  bnj1286  35175  bnj1408  35192  bnj1417  35197  r1omhf  35262  onvf1odlem4  35300  subfacp1lem5  35378  cvmsi  35459  gonar  35589  goalr  35591  mpst123  35734  mpstrcl  35735  msrrcl  35737  elmsta  35742  msubvrs  35754  elmpps  35767  elmthm  35770  bcprod  35932  dfon2lem4  35978  pprodss4v  36076  ivthALT  36529  neibastop2lem  36554  nnssi2  36649  nnssi3  36650  bj-sngltagi  37183  bj-elid5  37374  bj-fvmptunsn1  37462  bj-smgrpssmgmel  37474  bj-mndsssmgrpel  37476  bj-cmnssmndel  37478  bj-grpssmndel  37480  bj-ablssgrpel  37482  bj-ablsscmnel  37484  bj-vecssmodel  37487  bj-flddrng  37494  bj-rveccvec  37510  bj-rvecabl  37512  taupilemrplb  37525  icorempo  37556  elxp8  37576  sin2h  37811  cos2h  37812  tan2h  37813  poimirlem14  37835  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  poimirlem32  37853  mblfinlem1  37858  cnambfre  37869  dvtan  37871  itg2addnc  37875  itg2gt0cn  37876  ftc1cnnc  37893  ftc2nc  37903  dvasin  37905  dvacos  37906  cover2  37916  sstotbnd2  37975  heibor1lem  38010  heiborlem10  38021  opidonOLD  38053  exidcl  38077  rngosn3  38125  flddivrng  38200  toycom  39233  osumcllem7N  40222  pexmidlem4N  40233  diaintclN  41318  dibintclN  41427  mapd1o  41908  hdmapevec  42095  dvrelog2  42318  aks6d1c2lem4  42381  sticksstones1  42400  aks6d1c6lem5  42431  redvmptabs  42615  imacrhmcl  42769  prjspvs  42853  prjspeclsp  42855  0prjspnrel  42870  elrfi  42936  elrfirn  42937  elrfirn2  42938  mrefg3  42950  diophin  43014  diophun  43015  eq0rabdioph  43018  eqrabdioph  43019  pellex  43077  rmxycomplete  43159  jm2.23  43238  aomclem2  43297  fglmod  43315  lsmfgcl  43316  lmhmfgima  43326  lmhmfgsplit  43328  isnumbasabl  43348  dgrsub2  43377  itgocn  43406  areaquad  43458  cantnftermord  43562  omabs2  43574  nna1iscard  43786  elmapintrab  43817  corcltrcl  43980  k0004val0  44395  elscottab  44485  radcnvrat  44555  uzmptshftfval  44587  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  onfrALTlem2  44787  onfrALTlem2VD  45129  uzwo4  45298  mptssid  45485  uzublem  45674  eliccelioc  45767  elicores  45779  sqrlearg  45799  fsumiunss  45821  limcdm0  45864  sumnnodd  45876  fnlimfvre  45918  limsupubuzlem  45956  limsupmnflem  45964  limsupre3uzlem  45979  climuzlem  45987  liminflelimsuplem  46019  cncfshift  46118  cncfperiod  46123  icccncfext  46131  dvnprodlem1  46190  dvnprodlem2  46191  itgsin0pilem1  46194  itgsinexplem1  46198  itgsinexp  46199  ditgeqiooicc  46204  itgsubsticclem  46219  itgioocnicc  46221  itgsbtaddcnst  46226  stoweidlem34  46278  stoweidlem41  46285  stoweidlem51  46295  wallispilem2  46310  stirlinglem11  46328  dirkercncflem2  46348  fourierdlem5  46356  fourierdlem9  46360  fourierdlem17  46368  fourierdlem18  46369  fourierdlem20  46371  fourierdlem39  46390  fourierdlem48  46398  fourierdlem49  46399  fourierdlem62  46412  fourierdlem66  46416  fourierdlem68  46418  fourierdlem72  46422  fourierdlem73  46423  fourierdlem81  46431  fourierdlem83  46433  fourierdlem85  46435  fourierdlem87  46437  fourierdlem88  46438  fourierdlem92  46442  fourierdlem95  46445  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  etransclem24  46502  etransclem35  46513  etransclem37  46515  salexct  46578  salgencntex  46587  sge0resplit  46650  sge0split  46653  meaiuninclem  46724  caratheodorylem1  46770  volicorescl  46797  hoidmv1lelem3  46837  opnvonmbllem2  46877  ovolval2  46888  ovolval3  46891  ovolval4lem1  46893  ovolval4lem2  46894  sssmf  46982  smfaddlem1  47007  smflimlem2  47016  smfrec  47033  smfdiv  47041  smfsuplem1  47055  smfsuplem3  47057  et-ltneverrefl  47115  natglobalincr  47121  tannpoly  47136  fcores  47313  rehalfge1  47581  spr0el  47728  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbnd  48055  upgrimpthslem2  48154  stgredgiun  48204  isubgr3stgrlem7  48218  fldhmsubcALTV  48579  fvconst0ci  49136  fvconstdomi  49137  idfullsubc  49406  fulloppf  49408  fthoppf  49409  initopropdlemlem  49484