Theorem sseli 3941

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  sselii  3942  sselid  3943  elun1  4143  elun2  4144  elopabr  5546  elopabran  5547  elopaelxp  5752  copsex2ga  5795  imadifssran  6203  2elresin  6657  nfvres  6920  fvco4i  6984  mptrcl  7000  fvmptss  7003  fvmptex  7005  fvmptnf  7013  elfvmptrab1w  7018  elfvmptrab1  7019  fvopab4ndm  7021  fvimacnvi  7048  elpreima  7054  iinpreima  7065  ofrfvalg  7683  ofval  7686  off  7693  nnon  7867  finds  7892  finds2  7894  eqopi  8021  op1steq  8029  dfoprab4  8051  bropopvvv  8084  bropfvvvv  8086  reldmtpos  8229  smores2  8340  frsuc  8423  unifpw  9311  cantnfp1lem1  9646  cantnfp1lem3  9648  r1fin  9744  r1tr  9747  r1ordg  9749  r1ord3g  9750  r1val1  9757  tz9.12lem3  9760  tcrank  9855  elscottab  9869  cplem1  9874  hta  9882  tskwe  9935  cardprclem  9964  alephfplem3  10089  dfac12r  10129  ackbij1lem16  10216  ackbij2  10224  fin23lem28  10323  fin23lem30  10325  fin23lem31  10326  fin1a2lem6  10388  hsmexlem4  10412  hsmexlem5  10413  hsmexlem6  10414  axdc2lem  10431  axdc3lem2  10434  axcclem  10440  brdom5  10512  brdom4  10513  r1tskina  10766  gruina  10802  grur1a  10803  pinn  10862  0nnq  10908  elpqn  10909  recn  11189  rexr  11254  ltord1  11739  leord1  11740  eqord1  11741  nnre  12239  nncn  12240  nnind  12250  nnnn0  12510  nn0re  12512  nn0cn  12513  nn0xnn0  12580  nn0z  12614  uzuzle35  12910  nnq  12985  qcn  12986  rpre  13024  eliccxr  13461  difreicc  13510  iccshftri  13513  iccshftli  13515  iccdili  13517  icccntri  13519  fzval2  13537  fzelp1  13603  4fvwrd4  13675  elfzo1  13740  ico01fl0  13851  expcllem  14107  expcl2lem  14108  m1expcl2  14120  bcm1k  14350  bcpasc  14356  hashbclem  14488  wrdv  14565  pfxfv0  14728  pfxfvlsw  14731  cshimadifsn  14865  swrds2m  14977  01sqrexlem5  15296  cau3lem  15405  caubnd  15409  climconst2  15598  o1of2  15663  o1rlimmul  15669  caurcvg  15727  caucvg  15729  binomlem  15882  incexclem  15889  divcnvshft  15908  zprod  15990  fprodge1  16048  risefaccllem  16066  fallfaccllem  16067  bpolydiflem  16107  bpoly4  16112  dvdsflip  16374  divalglem8  16457  sadadd  16524  smumul  16550  isprm3  16740  phimullem  16837  prmdiveq  16844  unbenlem  16967  vdwnnlem1  17054  vdwnnlem3  17056  ramtcl2  17070  prmgaplem4  17113  cshwshashlem1  17154  structcnvcnv  17212  fvsetsid  17227  imasdsval2  17569  mreunirn  17652  mrcfval  17663  mrisval  17685  coapm  18127  tsrss  18644  chnccat  18681  ex-chn1  18692  submnd0  18820  smndex1id  18972  nmzsubg  19230  nmznsg  19233  cntzmhm  19410  symgtrinv  19541  pmtrdifellem4  19548  psgnpmtr  19579  efginvrel2  19796  efginvrel1  19797  efgsp1  19806  efgsres  19807  efgsfo  19808  frgpinv  19833  frgpupf  19842  frgpup1  19844  subcmn  19906  torsubg  19923  dprd2dlem1  20112  dpjidcl  20129  ablfaclem3  20158  nzrring  20598  lringnzr  20625  fldhmsubc  20865  acsfn1p  20879  lssacs  21065  cnsubdrglem  21536  rege0subm  21541  rge0srg  21556  zringunit  21584  znrrg  21683  psgnghm  21698  zrhpsgnevpm  21709  evpmodpmf1o  21714  pmtrodpm  21715  phlssphl  21777  frlmsslsp  21914  islinds4  21953  lmimlbs  21954  lbslcic  21959  psrbaglefi  22044  psrbagconf1o  22047  mplsubglem  22116  mplneg  22127  ressmpladd  22147  ressmplmul  22148  ressmplvsca  22149  mplmonmul  22155  psdmul  22297  ply1bascl  22331  mdetralt  22733  mdetunilem7  22743  chfacfpmmulgsum2  22990  tgval2  23081  ordtbas  23317  ordtrestixx  23347  hauslly  23617  kgentop  23667  ptbasin  23702  filunirn  24007  uzrest  24022  elflim  24096  flffval  24114  fclsval  24133  isfcls  24134  fcfval  24158  ustn0  24346  fmucndlem  24415  xmetunirn  24462  mopnval  24563  setsmstopn  24603  tmsval  24606  tngtopn  24775  qtopbaslem  24883  xrtgioo  24932  reperflem  24944  icccmplem1  24948  icopnfhmeo  25070  icccvx  25077  bndth  25085  pcoval1  25140  pcoval2  25143  pcoass  25151  pcorevlem  25153  pcorev2  25155  pi1xfrcnv  25184  csscld  25376  cfilfval  25391  caufval  25402  bcthlem1  25451  ivthlem1  25578  ivthlem3  25580  ovolicc2lem3  25646  ovolicc2lem4  25647  vitalilem1  25735  mbflimsup  25793  i1fd  25808  i1f0  25814  i1f1  25817  itg1addlem4  25826  itg1addlem5  25827  iblmbf  25894  ellimc2  26004  limcres  26013  limcun  26022  dvbsss  26029  perfdvf  26030  dvres2lem  26037  dvaddbr  26065  rolle  26117  cmvth  26118  dvlip  26120  dvlipcn  26121  dvle  26134  lhop1lem  26140  dvfsumle  26148  dvfsumge  26149  dvfsumabs  26150  dvfsumlem2  26154  ftc2  26171  itgparts  26174  itgsubstlem  26175  itgsubst  26176  deg1mul3  26241  coeval  26348  coeeu  26350  dgrval  26353  coef3  26357  coemulc  26380  dgrsub  26397  coecj  26403  coecjOLD  26405  dvply2  26415  dvnply  26417  quotval  26421  fta1  26437  plyexmo  26442  aacjcl  26456  taylfval  26487  dvtaylp  26498  abelth  26569  pilem3  26581  cos0pilt1  26662  sinord  26664  recosf1o  26665  resinf1o  26666  tanord1  26667  eff1olem  26678  dvloglem  26778  dvlog  26781  dvlog2lem  26782  advlogexp  26785  logtayl  26790  logtayl2  26792  dvcncxp1  26873  dvcnsqrt  26874  cxpcn3lem  26877  cxpcn3  26878  sqrtcn  26880  loglesqrt  26891  1cubr  26972  acosrecl  27033  efrlim  27099  jensen  27118  lgamgulmlem2  27159  lgamucov2  27168  basellem4  27213  musum  27320  mpodvdsmulf1o  27323  fsumdvdsmul  27324  dchrinvcl  27382  dchrghm  27385  dchrinv  27390  dchrsum2  27397  dchrsum  27398  rpvmasumlem  27616  dchrisum0lem2a  27646  pnt  27743  oldf  27995  madeno  28001  oldno  28002  newno  28003  oldmade  28026  leftold  28033  rightold  28034  leftno  28035  rightno  28036  addbdaylem  28175  addbday  28176  negsproplem2  28187  negsid  28199  negsunif  28213  mulsproplem12  28285  mulsproplem13  28286  mulsproplem14  28287  precsexlem11  28375  onno  28413  oncutlt  28422  n0no  28481  nnno  28482  nnn0s  28485  nnsgt0  28497  zno  28540  expscllem  28588  tglng  28780  axlowdimlem6  29237  axlowdimlem16  29247  axlowdimlem17  29248  axlowdim  29251  axeuclidlem  29252  axcontlem2  29255  axcontlem7  29260  axcontlem8  29261  nbusgrvtxm1uvtx  29695  wlk1walk  29928  pthdivtx  30016  pthdadjvtx  30017  crctcshwlkn0lem2  30100  crctcshwlkn0lem4  30102  clwwisshclwws  30306  fusgreg2wsp  30627  nvvcop  30886  nvex  30903  phnv  31106  sheli  31506  cheli  31524  hhssabloilem  31553  choc1  31619  shintcli  31621  chintcli  31623  shsleji  31662  pjini  31991  mayete3i  32020  dmadjop  32180  nlelshi  32352  cnlnadjeui  32369  cnlnssadj  32372  bdopadj  32374  pjimai  32468  stcl  32508  atelch  32636  fcnvgreu  32957  f1od2  33004  fcobijfs  33006  fcobijfs2  33007  uzssico  33069  iundisj2fi  33082  nnindf  33104  eliccioo  33190  gsummptres  33312  cyc3genpm  33412  elrspunidl  33679  0mplrim  33848  psrmonmul  33884  zarcls  34208  ordtrestNEW  34255  xrge0iifcnv  34267  xrge0iifcv  34268  xrge0iifiso  34269  xrge0iifhom  34271  qqhcn  34325  esumval  34380  gsumesum  34393  esumlub  34394  esumcst  34397  esumfsup  34404  issgon  34457  elrnsiga  34460  imambfm  34596  br2base  34603  sxbrsigalem0  34605  dya2iocucvr  34618  sxbrsigalem2  34620  sxbrsigalem5  34622  sxbrsiga  34624  omssubadd  34634  sitmcl  34685  oddpwdc  34688  eulerpartlemelr  34691  eulerpartlemgvv  34710  eulerpartlemgh  34712  eulerpartlemgs2  34714  eulerpartlemn  34715  sseqf  34726  ballotlem2  34823  ballotlemfp1  34826  ballotlemfc0  34827  ballotlemfcc  34828  ballotlemfmpn  34829  ballotlemsup  34839  ballotlemfrceq  34863  signswch  34892  rpsqrtcn  34924  prodfzo03  34934  itgexpif  34937  bnj1533  35184  bnj1137  35327  bnj1286  35351  bnj1408  35368  bnj1417  35373  r1omhf  35441  onvf1odlem4  35488  subfacp1lem5  35574  cvmsi  35655  gonar  35785  goalr  35787  mpst123  35930  mpstrcl  35931  msrrcl  35933  elmsta  35938  msubvrs  35950  elmpps  35963  elmthm  35966  bcprod  36128  dfon2lem4  36174  pprodss4v  36272  ivthALT  36734  neibastop2lem  36759  nnssi2  36854  nnssi3  36855  ttcel2  36900  bj-sngltagi  37505  bj-elid5  37700  bj-fvmptunsn1  37788  bj-smgrpssmgmel  37800  bj-mndsssmgrpel  37802  bj-cmnssmndel  37804  bj-grpssmndel  37806  bj-ablssgrpel  37808  bj-ablsscmnel  37810  bj-vecssmodel  37813  bj-flddrng  37820  bj-rveccvec  37836  bj-rvecabl  37838  taupilemrplb  37851  icorempo  37884  elxp8  37904  sin2h  38148  cos2h  38149  tan2h  38150  poimirlem14  38172  poimirlem26  38184  poimirlem27  38185  poimirlem31  38189  poimirlem32  38190  mblfinlem1  38195  cnambfre  38206  dvtan  38208  itg2addnc  38212  itg2gt0cn  38213  ftc1cnnc  38230  ftc2nc  38240  dvasin  38242  dvacos  38243  cover2  38253  sstotbnd2  38312  heibor1lem  38347  heiborlem10  38358  opidonOLD  38390  exidcl  38414  rngosn3  38462  flddivrng  38537  toycom  39636  osumcllem7N  40625  pexmidlem4N  40636  diaintclN  41721  dibintclN  41830  mapd1o  42311  hdmapevec  42498  dvrelog2  42720  aks6d1c2lem4  42783  sticksstones1  42802  aks6d1c6lem5  42833  redvmptabs  43010  imacrhmcl  43177  prjspvs  43233  prjspeclsp  43235  0prjspnrel  43250  elrfi  43316  elrfirn  43317  elrfirn2  43318  mrefg3  43330  diophin  43394  diophun  43395  eq0rabdioph  43398  eqrabdioph  43399  pellex  43453  rmxycomplete  43535  jm2.23  43614  aomclem2  43673  fglmod  43691  lsmfgcl  43692  lmhmfgima  43702  lmhmfgsplit  43704  isnumbasabl  43724  dgrsub2  43753  itgocn  43782  areaquad  43834  cantnftermord  43938  omabs2  43950  nna1iscard  44162  elmapintrab  44193  corcltrcl  44356  k0004val0  44771  radcnvrat  44915  uzmptshftfval  44947  binomcxplemdvsum  44956  binomcxplemnotnn0  44957  onfrALTlem2  45146  onfrALTlem2VD  45488  uzwo4  45664  mptssid  45847  uzublem  46035  eliccelioc  46128  elicores  46140  sqrlearg  46160  fsumiunss  46182  limcdm0  46225  sumnnodd  46237  fnlimfvre  46279  limsupubuzlem  46317  limsupmnflem  46325  limsupre3uzlem  46340  climuzlem  46348  liminflelimsuplem  46380  cncfshift  46479  cncfperiod  46484  icccncfext  46492  dvnprodlem1  46551  dvnprodlem2  46552  itgsin0pilem1  46555  itgsinexplem1  46559  itgsinexp  46560  ditgeqiooicc  46565  itgsubsticclem  46580  itgioocnicc  46582  itgsbtaddcnst  46587  stoweidlem34  46639  stoweidlem41  46646  stoweidlem51  46656  wallispilem2  46671  stirlinglem11  46689  dirkercncflem2  46709  fourierdlem5  46717  fourierdlem9  46721  fourierdlem17  46729  fourierdlem18  46730  fourierdlem20  46732  fourierdlem39  46751  fourierdlem48  46759  fourierdlem49  46760  fourierdlem62  46773  fourierdlem66  46777  fourierdlem68  46779  fourierdlem72  46783  fourierdlem73  46784  fourierdlem81  46792  fourierdlem83  46794  fourierdlem85  46796  fourierdlem87  46798  fourierdlem88  46799  fourierdlem92  46803  fourierdlem95  46806  fourierdlem103  46814  fourierdlem104  46815  fourierdlem112  46823  sqwvfoura  46833  sqwvfourb  46834  fouriersw  46836  etransclem24  46863  etransclem35  46874  etransclem37  46876  salexct  46939  salgencntex  46948  sge0resplit  47011  sge0split  47014  meaiuninclem  47085  caratheodorylem1  47131  volicorescl  47158  hoidmv1lelem3  47198  opnvonmbllem2  47238  ovolval2  47249  ovolval3  47252  ovolval4lem1  47254  ovolval4lem2  47255  smfaddlem1  47368  smflimlem2  47377  smfrec  47394  smfdiv  47402  smfsuplem1  47416  smfsuplem3  47418  et-ltneverrefl  47476  natglobalincr  47484  tannpoly  47515  fcores  47692  elfz2nn  47947  rehalfge1  47964  spr0el  48119  nprmdvdsfacm1lem4  48263  nprmdvdsfacm1  48264  ppivalnnnprmge6  48266  bgoldbtbndlem2  48459  bgoldbtbndlem3  48460  bgoldbtbnd  48462  upgrimpthslem2  48561  stgredgiun  48611  isubgr3stgrlem7  48625  fldhmsubcALTV  48986  fvconst0ci  49553  fvconstdomi  49554  idfullsubc  49823  fulloppf  49825  fthoppf  49826  initopropdlemlem  49901