Theorem sseli 3933

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3922

This theorem is referenced by:  sselii  3934  sselid  3935  elun1  4135  elun2  4136  elopabr  5545  elopabran  5546  elopaelxp  5751  copsex2ga  5794  imadifssran  6202  2elresin  6656  nfvres  6919  fvco4i  6983  mptrcl  6999  fvmptss  7002  fvmptex  7004  fvmptnf  7012  elfvmptrab1w  7017  elfvmptrab1  7018  fvopab4ndm  7020  fvimacnvi  7047  elpreima  7053  iinpreima  7064  ofrfvalg  7682  ofval  7685  off  7692  nnon  7864  finds  7889  finds2  7891  eqopi  8018  op1steq  8026  dfoprab4  8048  bropopvvv  8081  bropfvvvv  8083  reldmtpos  8226  smores2  8337  frsuc  8420  unifpw  9308  cantnfp1lem1  9643  cantnfp1lem3  9645  r1fin  9741  r1tr  9744  r1ordg  9746  r1ord3g  9747  r1val1  9754  tz9.12lem3  9757  tcrank  9852  elscottab  9866  cplem1  9871  hta  9879  tskwe  9932  cardprclem  9961  alephfplem3  10086  dfac12r  10126  ackbij1lem16  10213  ackbij2  10221  fin23lem28  10319  fin23lem30  10321  fin23lem31  10322  fin1a2lem6  10384  hsmexlem4  10408  hsmexlem5  10409  hsmexlem6  10410  axdc2lem  10427  axdc3lem2  10430  axcclem  10436  brdom5  10508  brdom4  10509  r1tskina  10762  gruina  10798  grur1a  10799  pinn  10858  0nnq  10904  elpqn  10905  recn  11185  rexr  11250  ltord1  11735  leord1  11736  eqord1  11737  nnre  12235  nncn  12236  nnind  12246  nnnn0  12506  nn0re  12508  nn0cn  12509  nn0xnn0  12576  nn0z  12610  uzuzle35  12906  nnq  12981  qcn  12982  rpre  13020  eliccxr  13457  difreicc  13506  iccshftri  13509  iccshftli  13511  iccdili  13513  icccntri  13515  fzval2  13533  fzelp1  13600  4fvwrd4  13672  elfzo1  13737  ico01fl0  13848  expcllem  14104  expcl2lem  14105  m1expcl2  14117  bcm1k  14347  bcpasc  14353  hashbclem  14485  wrdv  14562  pfxfv0  14725  pfxfvlsw  14728  cshimadifsn  14862  swrds2m  14974  01sqrexlem5  15293  cau3lem  15402  caubnd  15406  climconst2  15595  o1of2  15660  o1rlimmul  15666  caurcvg  15724  caucvg  15726  binomlem  15879  incexclem  15886  divcnvshft  15905  zprod  15987  fprodge1  16045  risefaccllem  16063  fallfaccllem  16064  bpolydiflem  16103  bpoly4  16108  dvdsflip  16370  divalglem8  16453  sadadd  16520  smumul  16546  isprm3  16736  phimullem  16833  prmdiveq  16840  unbenlem  16963  vdwnnlem1  17050  vdwnnlem3  17052  ramtcl2  17066  prmgaplem4  17109  cshwshashlem1  17150  structcnvcnv  17208  fvsetsid  17223  imasdsval2  17565  mreunirn  17648  mrcfval  17659  mrisval  17681  coapm  18123  tsrss  18640  chnccat  18677  ex-chn1  18688  submnd0  18816  smndex1id  18968  nmzsubg  19226  nmznsg  19229  cntzmhm  19406  symgtrinv  19537  pmtrdifellem4  19544  psgnpmtr  19575  efginvrel2  19792  efginvrel1  19793  efgsp1  19802  efgsres  19803  efgsfo  19804  frgpinv  19829  frgpupf  19838  frgpup1  19840  subcmn  19902  torsubg  19919  dprd2dlem1  20108  dpjidcl  20125  ablfaclem3  20154  nzrring  20613  lringnzr  20640  fldhmsubc  20888  acsfn1p  20902  lssacs  21088  cnsubdrglem  21568  rege0subm  21573  rge0srg  21588  zringunit  21616  znrrg  21715  psgnghm  21730  zrhpsgnevpm  21741  evpmodpmf1o  21746  pmtrodpm  21747  phlssphl  21809  frlmsslsp  21946  islinds4  21985  lmimlbs  21986  lbslcic  21991  psrbaglefi  22076  psrbagconf1o  22079  mplsubglem  22148  mplneg  22159  ressmpladd  22179  ressmplmul  22180  ressmplvsca  22181  mplmonmul  22187  psdmul  22329  ply1bascl  22363  mdetralt  22765  mdetunilem7  22775  chfacfpmmulgsum2  23022  tgval2  23113  ordtbas  23349  ordtrestixx  23379  hauslly  23649  kgentop  23699  ptbasin  23734  filunirn  24039  uzrest  24054  elflim  24128  flffval  24146  fclsval  24165  isfcls  24166  fcfval  24190  ustn0  24378  fmucndlem  24447  xmetunirn  24494  mopnval  24595  setsmstopn  24635  tmsval  24638  tngtopn  24807  qtopbaslem  24915  xrtgioo  24964  reperflem  24976  icccmplem1  24980  icopnfhmeo  25102  icccvx  25109  bndth  25117  pcoval1  25172  pcoval2  25175  pcoass  25183  pcorevlem  25185  pcorev2  25187  pi1xfrcnv  25216  csscld  25408  cfilfval  25423  caufval  25434  bcthlem1  25483  ivthlem1  25610  ivthlem3  25612  ovolicc2lem3  25678  ovolicc2lem4  25679  vitalilem1  25767  mbflimsup  25825  i1fd  25840  i1f0  25846  i1f1  25849  itg1addlem4  25858  itg1addlem5  25859  iblmbf  25926  ellimc2  26036  limcres  26045  limcun  26054  dvbsss  26061  perfdvf  26062  dvres2lem  26069  dvaddbr  26097  rolle  26149  cmvth  26150  dvlip  26152  dvlipcn  26153  dvle  26166  lhop1lem  26172  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvfsumlem2  26186  ftc2  26203  itgparts  26206  itgsubstlem  26207  itgsubst  26208  deg1mul3  26273  coeval  26380  coeeu  26382  dgrval  26385  coef3  26389  coemulc  26412  dgrsub  26429  coecj  26435  coecjOLD  26437  dvply2  26447  dvnply  26449  quotval  26453  fta1  26469  plyexmo  26474  aacjcl  26490  taylfval  26522  dvtaylp  26533  abelth  26604  pilem3  26616  cos0pilt1  26697  sinord  26699  recosf1o  26700  resinf1o  26701  tanord1  26702  eff1olem  26713  dvloglem  26813  dvlog  26816  dvlog2lem  26817  advlogexp  26820  logtayl  26825  logtayl2  26827  dvcncxp1  26908  dvcnsqrt  26909  cxpcn3lem  26912  cxpcn3  26913  sqrtcn  26915  loglesqrt  26926  1cubr  27007  acosrecl  27068  efrlim  27134  jensen  27153  lgamgulmlem2  27194  lgamucov2  27203  basellem4  27248  musum  27355  mpodvdsmulf1o  27358  fsumdvdsmul  27359  dchrinvcl  27417  dchrghm  27420  dchrinv  27425  dchrsum2  27432  dchrsum  27433  rpvmasumlem  27651  dchrisum0lem2a  27681  pnt  27778  oldf  28030  madeno  28036  oldno  28037  newno  28038  oldmade  28061  leftold  28068  rightold  28069  leftno  28070  rightno  28071  addbdaylem  28210  addbday  28211  negsproplem2  28222  negsid  28234  negsunif  28248  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  precsexlem11  28410  onno  28448  oncutlt  28457  n0no  28516  nnno  28517  nnn0s  28520  nnsgt0  28532  zno  28575  expscllem  28623  tglng  28815  axlowdimlem6  29297  axlowdimlem16  29307  axlowdimlem17  29308  axlowdim  29311  axeuclidlem  29312  axcontlem2  29315  axcontlem7  29320  axcontlem8  29321  nbusgrvtxm1uvtx  29755  wlk1walk  29988  pthdivtx  30076  pthdadjvtx  30077  crctcshwlkn0lem2  30160  crctcshwlkn0lem4  30162  clwwisshclwws  30366  fusgreg2wsp  30687  nvvcop  30946  nvex  30963  phnv  31166  sheli  31566  cheli  31584  hhssabloilem  31613  choc1  31679  shintcli  31681  chintcli  31683  shsleji  31722  pjini  32051  mayete3i  32080  dmadjop  32240  nlelshi  32412  cnlnadjeui  32429  cnlnssadj  32432  bdopadj  32434  pjimai  32528  stcl  32568  atelch  32696  fcnvgreu  33017  f1od2  33064  fcobijfs  33066  fcobijfs2  33067  uzssico  33129  iundisj2fi  33142  nnindf  33164  eliccioo  33250  gsummptres  33372  cyc3genpm  33472  elrspunidl  33736  0mplrim  33904  psrmonmul  33940  zarcls  34264  ordtrestNEW  34311  xrge0iifcnv  34323  xrge0iifcv  34324  xrge0iifiso  34325  xrge0iifhom  34327  qqhcn  34381  esumval  34436  gsumesum  34449  esumlub  34450  esumcst  34453  esumfsup  34460  issgon  34513  elrnsiga  34516  imambfm  34652  br2base  34659  sxbrsigalem0  34661  dya2iocucvr  34674  sxbrsigalem2  34676  sxbrsigalem5  34678  sxbrsiga  34680  omssubadd  34690  sitmcl  34741  oddpwdc  34744  eulerpartlemelr  34747  eulerpartlemgvv  34766  eulerpartlemgh  34768  eulerpartlemgs2  34770  eulerpartlemn  34771  sseqf  34782  ballotlem2  34879  ballotlemfp1  34882  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemfmpn  34885  ballotlemsup  34895  ballotlemfrceq  34919  signswch  34948  rpsqrtcn  34980  prodfzo03  34990  itgexpif  34993  bnj1533  35240  bnj1137  35383  bnj1286  35407  bnj1408  35424  bnj1417  35429  r1omhf  35500  onvf1odlem4  35590  subfacp1lem5  35676  cvmsi  35757  gonar  35887  goalr  35889  mpst123  36032  mpstrcl  36033  msrrcl  36035  elmsta  36040  msubvrs  36052  elmpps  36065  elmthm  36068  bcprod  36230  dfon2lem4  36276  pprodss4v  36374  ivthALT  36846  neibastop2lem  36871  nnssi2  36966  nnssi3  36967  ttcel2  37012  bj-sngltagi  37618  bj-elid5  37813  bj-fvmptunsn1  37901  bj-smgrpssmgmel  37913  bj-mndsssmgrpel  37915  bj-cmnssmndel  37917  bj-grpssmndel  37919  bj-ablssgrpel  37921  bj-ablsscmnel  37923  bj-vecssmodel  37926  bj-flddrng  37933  bj-rveccvec  37949  bj-rvecabl  37951  taupilemrplb  37964  icorempo  37997  elxp8  38017  sin2h  38261  cos2h  38262  tan2h  38263  poimirlem14  38285  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  mblfinlem1  38308  cnambfre  38319  dvtan  38321  itg2addnc  38325  itg2gt0cn  38326  ftc1cnnc  38343  ftc2nc  38353  dvasin  38355  dvacos  38356  cover2  38366  sstotbnd2  38425  heibor1lem  38460  heiborlem10  38471  opidonOLD  38503  exidcl  38527  rngosn3  38575  flddivrng  38650  toycom  39747  osumcllem7N  40736  pexmidlem4N  40747  diaintclN  41832  dibintclN  41941  mapd1o  42422  hdmapevec  42609  dvrelog2  42831  aks6d1c2lem4  42894  sticksstones1  42913  aks6d1c6lem5  42944  redvmptabs  43121  imacrhmcl  43288  prjspvs  43342  prjspeclsp  43344  0prjspnrel  43359  elrfi  43425  elrfirn  43426  elrfirn2  43427  mrefg3  43439  diophin  43503  diophun  43504  eq0rabdioph  43507  eqrabdioph  43508  pellex  43562  rmxycomplete  43644  jm2.23  43723  aomclem2  43782  fglmod  43800  lsmfgcl  43801  lmhmfgima  43811  lmhmfgsplit  43813  isnumbasabl  43833  dgrsub2  43862  itgocn  43891  areaquad  43943  cantnftermord  44047  omabs2  44059  nna1iscard  44271  elmapintrab  44302  corcltrcl  44465  k0004val0  44880  radcnvrat  45024  uzmptshftfval  45056  binomcxplemdvsum  45065  binomcxplemnotnn0  45066  onfrALTlem2  45255  onfrALTlem2VD  45597  uzwo4  45773  mptssid  45956  uzublem  46144  eliccelioc  46237  elicores  46249  sqrlearg  46269  fsumiunss  46291  limcdm0  46334  sumnnodd  46346  fnlimfvre  46388  limsupubuzlem  46426  limsupmnflem  46434  limsupre3uzlem  46449  climuzlem  46457  liminflelimsuplem  46489  cncfshift  46588  cncfperiod  46593  icccncfext  46601  dvnprodlem1  46660  dvnprodlem2  46661  itgsin0pilem1  46664  itgsinexplem1  46668  itgsinexp  46669  ditgeqiooicc  46674  itgsubsticclem  46689  itgioocnicc  46691  itgsbtaddcnst  46696  stoweidlem34  46748  stoweidlem41  46755  stoweidlem51  46765  wallispilem2  46780  stirlinglem11  46798  dirkercncflem2  46818  fourierdlem5  46826  fourierdlem9  46830  fourierdlem17  46838  fourierdlem18  46839  fourierdlem20  46841  fourierdlem39  46860  fourierdlem48  46868  fourierdlem49  46869  fourierdlem62  46882  fourierdlem66  46886  fourierdlem68  46888  fourierdlem72  46892  fourierdlem73  46893  fourierdlem81  46901  fourierdlem83  46903  fourierdlem85  46905  fourierdlem87  46907  fourierdlem88  46908  fourierdlem92  46912  fourierdlem95  46915  fourierdlem103  46923  fourierdlem104  46924  fourierdlem112  46932  sqwvfoura  46942  sqwvfourb  46943  fouriersw  46945  etransclem24  46972  etransclem35  46983  etransclem37  46985  salexct  47048  salgencntex  47057  sge0resplit  47120  sge0split  47123  meaiuninclem  47194  caratheodorylem1  47240  volicorescl  47267  hoidmv1lelem3  47307  opnvonmbllem2  47347  ovolval2  47358  ovolval3  47361  ovolval4lem1  47363  ovolval4lem2  47364  smfaddlem1  47477  smflimlem2  47486  smfrec  47503  smfdiv  47511  smfsuplem1  47525  smfsuplem3  47527  et-ltneverrefl  47585  natglobalincr  47593  tannpoly  47627  fcores  47804  elfz2nn  48059  rehalfge1  48076  spr0el  48231  nprmdvdsfacm1lem4  48375  nprmdvdsfacm1  48376  ppivalnnnprmge6  48378  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbnd  48574  upgrimpthslem2  48673  stgredgiun  48723  isubgr3stgrlem7  48737  fldhmsubcALTV  49098  fvconst0ci  49669  fvconstdomi  49670  idfullsubc  49939  fulloppf  49941  fthoppf  49942  initopropdlemlem  50017