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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951

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 2007  ax-8 2110

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

This theorem is referenced by:  sselii  3980  sselid  3981  elun1  4182  elun2  4183  elopabr  5566  elopabran  5567  elopaelxp  5775  copsex2ga  5817  2elresin  6689  nfvres  6947  fvco4i  7010  mptrcl  7025  fvmptss  7028  fvmptex  7030  fvmptnf  7038  elfvmptrab1w  7043  elfvmptrab1  7044  fvopab4ndm  7046  fvimacnvi  7072  elpreima  7078  iinpreima  7089  ofrfvalg  7705  ofval  7708  off  7715  nnon  7893  finds  7918  finds2  7920  eqopi  8050  op1steq  8058  dfoprab4  8080  bropopvvv  8115  bropfvvvv  8117  reldmtpos  8259  wfrlem10OLD  8358  smores2  8394  frsuc  8477  unifpw  9395  cantnfp1lem1  9718  cantnfp1lem3  9720  r1fin  9813  r1tr  9816  r1ordg  9818  r1ord3g  9819  r1val1  9826  tz9.12lem3  9829  tcrank  9924  cplem1  9929  hta  9937  tskwe  9990  cardprclem  10019  alephfplem3  10146  dfac12r  10187  ackbij1lem16  10274  ackbij2  10282  fin23lem28  10380  fin23lem30  10382  fin23lem31  10383  fin1a2lem6  10445  hsmexlem4  10469  hsmexlem5  10470  hsmexlem6  10471  axdc2lem  10488  axdc3lem2  10491  axcclem  10497  brdom5  10569  brdom4  10570  r1tskina  10822  gruina  10858  grur1a  10859  pinn  10918  0nnq  10964  elpqn  10965  recn  11245  rexr  11307  ltord1  11789  leord1  11790  eqord1  11791  nnre  12273  nncn  12274  nnind  12284  nnnn0  12533  nn0re  12535  nn0cn  12536  nn0xnn0  12603  nnzOLD  12637  nn0z  12638  nnq  13004  qcn  13005  rpre  13043  eliccxr  13475  difreicc  13524  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  fzval2  13550  fzelp1  13616  4fvwrd4  13688  elfzo1  13752  ico01fl0  13859  expcllem  14113  expcl2lem  14114  m1expcl2  14126  bcm1k  14354  bcpasc  14360  hashbclem  14491  wrdv  14567  pfxfv0  14730  pfxfvlsw  14733  cshimadifsn  14868  swrds2m  14980  01sqrexlem5  15285  cau3lem  15393  caubnd  15397  climconst2  15584  o1of2  15649  o1rlimmul  15655  caurcvg  15713  caucvg  15715  binomlem  15865  incexclem  15872  divcnvshft  15891  zprod  15973  fprodge1  16031  risefaccllem  16049  fallfaccllem  16050  bpolydiflem  16090  bpoly4  16095  dvdsflip  16354  divalglem8  16437  sadadd  16504  smumul  16530  isprm3  16720  phimullem  16816  prmdiveq  16823  unbenlem  16946  vdwnnlem1  17033  vdwnnlem3  17035  ramtcl2  17049  prmgaplem4  17092  cshwshashlem1  17133  structcnvcnv  17190  fvsetsid  17205  imasdsval2  17561  mreunirn  17644  mrcfval  17651  mrisval  17673  coapm  18116  tsrss  18634  submnd0  18776  smndex1id  18924  nmzsubg  19183  nmznsg  19186  cntzmhm  19359  symgtrinv  19490  pmtrdifellem4  19497  psgnpmtr  19528  efginvrel2  19745  efginvrel1  19746  efgsp1  19755  efgsres  19756  efgsfo  19757  frgpinv  19782  frgpupf  19791  frgpup1  19793  subcmn  19855  torsubg  19872  dprd2dlem1  20061  dpjidcl  20078  ablfaclem3  20107  nzrring  20516  lringnzr  20541  fldhmsubc  20786  acsfn1p  20800  lssacs  20965  cnsubdrglem  21436  rege0subm  21441  rge0srg  21456  zringunit  21477  znrrg  21584  psgnghm  21598  zrhpsgnevpm  21609  evpmodpmf1o  21614  pmtrodpm  21615  phlssphl  21677  frlmsslsp  21816  islinds4  21855  lmimlbs  21856  lbslcic  21861  psrbaglefi  21946  psrbagconf1o  21949  mplsubglem  22019  mplneg  22030  ressmpladd  22047  ressmplmul  22048  ressmplvsca  22049  mplmonmul  22054  psdmul  22170  ply1bascl  22205  mdetralt  22614  mdetunilem7  22624  chfacfpmmulgsum2  22871  tgval2  22963  ordtbas  23200  ordtrestixx  23230  hauslly  23500  kgentop  23550  ptbasin  23585  filunirn  23890  uzrest  23905  elflim  23979  flffval  23997  fclsval  24016  isfcls  24017  fcfval  24041  ustn0  24229  fmucndlem  24300  xmetunirn  24347  mopnval  24448  setsmstopn  24490  tmsval  24493  tngtopn  24671  qtopbaslem  24779  xrtgioo  24828  reperflem  24840  icccmplem1  24844  icopnfhmeo  24974  icccvx  24981  bndth  24990  reparphtiOLD  25030  pcoval1  25046  pcoval2  25049  pcoass  25057  pcorevlem  25059  pcorev2  25061  pi1xfrcnv  25090  csscld  25283  cfilfval  25298  caufval  25309  bcthlem1  25358  ivthlem1  25486  ivthlem3  25488  ovolicc2lem3  25554  ovolicc2lem4  25555  vitalilem1  25643  mbflimsup  25701  i1fd  25716  i1f0  25722  i1f1  25725  itg1addlem4  25734  itg1addlem5  25735  iblmbf  25802  ellimc2  25912  limcres  25921  limcun  25930  dvbsss  25937  perfdvf  25938  dvres2lem  25945  dvaddbr  25974  rolle  26028  cmvth  26029  cmvthOLD  26030  dvlip  26032  dvlipcn  26033  dvle  26046  lhop1lem  26052  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc2  26085  itgparts  26088  itgsubstlem  26089  itgsubst  26090  deg1mul3  26155  coeval  26262  coeeu  26264  dgrval  26267  coef3  26271  coemulc  26294  dgrsub  26312  coecj  26318  coecjOLD  26320  dvply2  26328  dvnply  26330  quotval  26334  fta1  26350  plyexmo  26355  aacjcl  26369  taylfval  26400  dvtaylp  26412  abelth  26485  pilem3  26497  cos0pilt1  26574  sinord  26576  recosf1o  26577  resinf1o  26578  tanord1  26579  eff1olem  26590  dvloglem  26690  dvlog  26693  dvlog2lem  26694  advlogexp  26697  logtayl  26702  logtayl2  26704  dvcncxp1  26785  dvcnsqrt  26786  cxpcn3lem  26790  cxpcn3  26791  sqrtcn  26793  loglesqrt  26804  1cubr  26885  acosrecl  26946  efrlim  27012  efrlimOLD  27013  jensen  27032  lgamgulmlem2  27073  lgamucov2  27082  basellem4  27127  musum  27234  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dchrinvcl  27297  dchrghm  27300  dchrinv  27305  dchrsum2  27312  dchrsum  27313  rpvmasumlem  27531  dchrisum0lem2a  27561  pnt  27658  oldf  27896  leftirr  27929  rightirr  27930  lrold  27935  sltlpss  27945  addsproplem2  28003  sleadd1  28022  addsuniflem  28034  addsbdaylem  28049  addsbday  28050  negsproplem2  28061  negsid  28073  negsunif  28087  mulsrid  28139  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  precsexlem9  28239  precsexlem11  28241  onsno  28278  onaddscl  28286  onmulscl  28287  n0sno  28328  nnsno  28329  nnn0s  28332  nnsgt0  28342  zno  28368  tglng  28554  axlowdimlem6  28962  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  axeuclidlem  28977  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  nbusgrvtxm1uvtx  29422  wlk1walk  29657  pthdivtx  29747  pthdadjvtx  29748  crctcshwlkn0lem2  29831  crctcshwlkn0lem4  29833  clwwisshclwws  30034  fusgreg2wsp  30355  nvvcop  30613  nvex  30630  phnv  30833  sheli  31233  cheli  31251  hhssabloilem  31280  choc1  31346  shintcli  31348  chintcli  31350  shsleji  31389  pjini  31718  mayete3i  31747  dmadjop  31907  nlelshi  32079  cnlnadjeui  32096  cnlnssadj  32099  bdopadj  32101  pjimai  32195  stcl  32235  atelch  32363  fcnvgreu  32683  f1od2  32732  fcobijfs  32734  uzssico  32786  iundisj2fi  32799  nnindf  32821  eliccioo  32913  gsummptres  33055  cyc3genpm  33172  elrspunidl  33456  zarcls  33873  ordtrestNEW  33920  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  qqhcn  33992  esumval  34047  gsumesum  34060  esumlub  34061  esumcst  34064  esumfsup  34071  issgon  34124  elrnsiga  34127  imambfm  34264  br2base  34271  sxbrsigalem0  34273  dya2iocucvr  34286  sxbrsigalem2  34288  sxbrsigalem5  34290  sxbrsiga  34292  omssubadd  34302  sitmcl  34353  oddpwdc  34356  eulerpartlemelr  34359  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemgs2  34382  eulerpartlemn  34383  sseqf  34394  ballotlem2  34491  ballotlemfp1  34494  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemfmpn  34497  ballotlemsup  34507  ballotlemfrceq  34531  signswch  34576  rpsqrtcn  34608  prodfzo03  34618  itgexpif  34621  bnj1533  34866  bnj1137  35009  bnj1286  35033  bnj1408  35050  bnj1417  35055  subfacp1lem5  35189  cvmsi  35270  gonar  35400  goalr  35402  mpst123  35545  mpstrcl  35546  msrrcl  35548  elmsta  35553  msubvrs  35565  elmpps  35578  elmthm  35581  bcprod  35738  dfon2lem4  35787  pprodss4v  35885  ivthALT  36336  neibastop2lem  36361  nnssi2  36456  nnssi3  36457  bj-sngltagi  36983  bj-elid5  37170  bj-fvmptunsn1  37258  bj-smgrpssmgmel  37270  bj-mndsssmgrpel  37272  bj-cmnssmndel  37274  bj-grpssmndel  37276  bj-ablssgrpel  37278  bj-ablsscmnel  37280  bj-vecssmodel  37283  bj-flddrng  37290  bj-rveccvec  37306  bj-rvecabl  37308  taupilemrplb  37321  icorempo  37352  elxp8  37372  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem14  37641  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  mblfinlem1  37664  cnambfre  37675  dvtan  37677  itg2addnc  37681  itg2gt0cn  37682  ftc1cnnc  37699  ftc2nc  37709  dvasin  37711  dvacos  37712  cover2  37722  sstotbnd2  37781  heibor1lem  37816  heiborlem10  37827  opidonOLD  37859  exidcl  37883  rngosn3  37931  flddivrng  38006  toycom  38974  osumcllem7N  39964  pexmidlem4N  39975  diaintclN  41060  dibintclN  41169  mapd1o  41650  hdmapevec  41837  dvrelog2  42065  aks6d1c2lem4  42128  sticksstones1  42147  aks6d1c6lem5  42178  redvmptabs  42390  imacrhmcl  42524  prjspvs  42620  prjspeclsp  42622  0prjspnrel  42637  elrfi  42705  elrfirn  42706  elrfirn2  42707  mrefg3  42719  diophin  42783  diophun  42784  eq0rabdioph  42787  eqrabdioph  42788  pellex  42846  rmxycomplete  42929  jm2.23  43008  aomclem2  43067  fglmod  43085  lsmfgcl  43086  lmhmfgima  43096  lmhmfgsplit  43098  isnumbasabl  43118  dgrsub2  43147  itgocn  43176  areaquad  43228  cantnftermord  43333  omabs2  43345  nna1iscard  43558  elmapintrab  43589  corcltrcl  43752  k0004val0  44167  elscottab  44263  radcnvrat  44333  uzmptshftfval  44365  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  onfrALTlem2  44566  onfrALTlem2VD  44909  uzwo4  45058  mptssid  45247  uzublem  45441  eliccelioc  45534  elicores  45546  sqrlearg  45566  fsumiunss  45590  limcdm0  45633  sumnnodd  45645  fnlimfvre  45689  limsupubuzlem  45727  limsupmnflem  45735  limsupre3uzlem  45750  climuzlem  45758  cncfshift  45889  cncfperiod  45894  icccncfext  45902  dvnprodlem1  45961  dvnprodlem2  45962  itgsin0pilem1  45965  itgsinexplem1  45969  itgsinexp  45970  ditgeqiooicc  45975  itgsubsticclem  45990  itgioocnicc  45992  itgsbtaddcnst  45997  stoweidlem34  46049  stoweidlem41  46056  stoweidlem51  46066  wallispilem2  46081  stirlinglem11  46099  dirkercncflem2  46119  fourierdlem5  46127  fourierdlem9  46131  fourierdlem17  46139  fourierdlem18  46140  fourierdlem20  46142  fourierdlem39  46161  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem66  46187  fourierdlem68  46189  fourierdlem72  46193  fourierdlem73  46194  fourierdlem81  46202  fourierdlem83  46204  fourierdlem85  46206  fourierdlem87  46208  fourierdlem88  46209  fourierdlem92  46213  fourierdlem95  46216  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  etransclem24  46273  etransclem35  46284  etransclem37  46286  salexct  46349  salgencntex  46358  sge0resplit  46421  sge0split  46424  meaiuninclem  46495  caratheodorylem1  46541  volicorescl  46568  hoidmv1lelem3  46608  opnvonmbllem2  46648  ovolval2  46659  ovolval3  46662  ovolval4lem1  46664  ovolval4lem2  46665  pimiooltgt  46725  sssmf  46753  smfaddlem1  46778  smflimlem2  46787  smfrec  46804  smfdiv  46812  smfsuplem1  46826  smfsuplem3  46828  et-ltneverrefl  46886  natglobalincr  46892  fcores  47079  spr0el  47469  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  stgredgiun  47925  isubgr3stgrlem7  47939  fldhmsubcALTV  48249  fvconst0ci  48790  fvconstdomi  48791