Theorem sseli 3930

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837  df-ss 3919

This theorem is used by:  sselii  3931  sselid  3932  elun1  4131  elun2  4132  elopabr  5543  elopabran  5544  elopaelxp  5749  copsex2ga  5792  imadifssran  6201  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  7066  ofrfvalg  7690  ofval  7693  off  7700  nnon  7872  finds  7897  finds2  7899  eqopi  8026  op1steq  8034  dfoprab4  8056  bropopvvv  8091  bropfvvvv  8093  reldmtpos  8236  smores2  8347  frsuc  8430  unifpw  9326  cantnfp1lem1  9661  cantnfp1lem3  9663  r1fin  9759  r1tr  9762  r1ordg  9764  r1ord3g  9765  r1val1  9772  tz9.12lem3  9775  tcrank  9870  elscottab  9885  cplem1  9893  cplem1OLD  9894  hta  9905  htaOLD  9906  tskwe  9959  cardprclem  9988  alephfplem3  10113  dfac12r  10153  ackbij1lem16  10240  ackbij2  10248  fin23lem28  10346  fin23lem30  10348  fin23lem31  10349  fin1a2lem6  10411  hsmexlem4  10435  hsmexlem5  10436  hsmexlem6  10437  axdc2lem  10454  axdc3lem2  10457  axcclem  10463  brdom5  10536  brdom4  10537  r1tskina  10795  gruina  10831  grur1a  10832  pinn  10891  0nnq  10937  elpqn  10938  recn  11218  rexr  11283  ltord1  11768  leord1  11769  eqord1  11770  nnre  12268  nncn  12269  nnind  12279  nnnn0  12539  nn0re  12541  nn0cn  12542  nn0xnn0  12609  nn0z  12643  uzuzle35  12940  nnq  13015  qcn  13016  rpre  13055  eliccxr  13492  difreicc  13541  iccshftri  13544  iccshftli  13546  iccdili  13548  icccntri  13550  fzval2  13568  fzelp1  13635  4fvwrd4  13707  elfzo1  13772  ico01fl0  13884  expcllem  14140  expcl2lem  14141  m1expcl2  14153  bcm1k  14383  bcpasc  14389  hashbclem  14521  wrdv  14598  pfxfv0  14765  pfxfvlsw  14768  cshimadifsn  14904  swrds2m  15016  01sqrexlem5  15337  cau3lem  15446  caubnd  15450  climconst2  15639  o1of2  15704  o1rlimmul  15710  caurcvg  15768  caucvg  15770  binomlem  15922  incexclem  15929  divcnvshft  15948  zprod  16030  fprodge1  16088  risefaccllem  16106  fallfaccllem  16107  bpolydiflem  16146  bpoly4  16151  dvdsflip  16413  divalglem8  16496  sadadd  16563  smumul  16589  isprm3  16779  phimullem  16876  prmdiveq  16883  unbenlem  17006  vdwnnlem1  17093  vdwnnlem3  17095  ramtcl2  17109  prmgaplem4  17152  cshwshashlem1  17193  structcnvcnv  17251  fvsetsid  17266  imasdsval2  17608  mreunirn  17691  mrcfval  17702  mrisval  17724  coapm  18166  tsrss  18683  chnccat  18720  ex-chn1  18731  submnd0OLD  18876  smndex1id  19029  nmzsubg  19294  nmznsg  19297  cntzmhm  19474  symgtrinv  19605  pmtrdifellem4  19612  psgnpmtr  19643  efginvrel2  19860  efginvrel1  19861  efgsp1  19870  efgsres  19871  efgsfo  19872  frgpinv  19897  frgpupf  19906  frgpup1  19908  subcmn  19970  torsubg  19987  dprd2dlem1  20176  dpjidcl  20193  ablfaclem3  20222  nzrring  20682  lringnzr  20709  fldhmsubc  20957  acsfn1p  20971  lssacs  21157  cnsubdrglem  21637  rege0subm  21642  rge0srg  21657  zringunit  21685  znrrg  21784  psgnghm  21799  zrhpsgnevpm  21810  evpmodpmf1o  21815  pmtrodpm  21816  phlssphl  21878  frlmsslsp  22015  islinds4  22054  lmimlbs  22055  lbslcic  22060  psrbaglefi  22147  psrbagconf1o  22150  mplsubglem  22219  mplneg  22230  ressmpladd  22250  ressmplmul  22251  ressmplvsca  22252  mplmonmul  22258  psdmul  22400  ply1bascl  22434  mdetralt  22836  mdetunilem7  22846  chfacfpmmulgsum2  23096  tgval2  23187  ordtbas  23423  ordtrestixx  23453  hauslly  23724  kgentop  23774  ptbasin  23809  filunirn  24114  uzrest  24129  elflim  24203  flffval  24221  fclsval  24240  isfcls  24241  fcfval  24265  ustn0  24453  fmucndlem  24522  xmetunirn  24569  mopnval  24670  setsmstopn  24710  tmsval  24713  tngtopn  24882  qtopbaslem  24990  xrtgioo  25039  reperflem  25051  icccmplem1  25055  icopnfhmeo  25177  icccvx  25184  bndth  25192  pcoval1  25247  pcoval2  25250  pcoass  25258  pcorevlem  25260  pcorev2  25262  pi1xfrcnv  25291  csscld  25483  cfilfval  25498  caufval  25509  bcthlem1  25558  ivthlem1  25685  ivthlem3  25687  ovolicc2lem3  25753  ovolicc2lem4  25754  vitalilem1  25842  mbflimsup  25900  i1fd  25915  i1f0  25921  i1f1  25924  itg1addlem4  25933  itg1addlem5  25934  iblmbf  26001  ellimc2  26111  limcres  26120  limcun  26129  dvbsss  26136  perfdvf  26137  dvres2lem  26144  dvaddbr  26172  rolle  26224  cmvth  26225  dvlip  26227  dvlipcn  26228  dvle  26241  lhop1lem  26247  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  dvfsumlem2  26261  ftc2  26278  itgparts  26281  itgsubstlem  26282  itgsubst  26283  deg1mul3  26348  coeval  26456  coeeu  26458  dgrval  26461  coef3  26465  coemulc  26488  dgrsub  26505  coecj  26511  coecjOLD  26513  dvply2  26523  dvnply  26525  quotval  26529  fta1  26545  plyexmo  26552  aacjcl  26570  taylfval  26602  dvtaylp  26613  abelth  26684  pilem3  26696  cos0pilt1  26777  sinord  26779  recosf1o  26780  resinf1o  26781  tanord1  26782  eff1olem  26793  dvloglem  26893  dvlog  26896  dvlog2lem  26897  advlogexp  26900  logtayl  26905  logtayl2  26907  dvcncxp1  26988  dvcnsqrt  26989  cxpcn3lem  26992  cxpcn3  26993  sqrtcn  26995  loglesqrt  27006  1cubr  27087  acosrecl  27148  efrlim  27214  jensen  27233  lgamgulmlem2  27274  lgamucov2  27283  basellem4  27328  musum  27435  mpodvdsmulf1o  27438  fsumdvdsmul  27439  dchrinvcl  27497  dchrghm  27500  dchrinv  27505  dchrsum2  27512  dchrsum  27513  rpvmasumlem  27731  dchrisum0lem2a  27761  pnt  27858  oldf  28110  madeno  28116  oldno  28117  newno  28118  oldmade  28141  leftold  28148  rightold  28149  leftno  28150  rightno  28151  addbdaylem  28290  addbday  28291  negsproplem2  28302  negsid  28314  negsunif  28328  mulsproplem12  28400  mulsproplem13  28401  mulsproplem14  28402  precsexlem11  28490  onno  28528  oncutlt  28537  n0no  28596  nnno  28597  nnn0s  28600  nnsgt0  28612  zno  28655  expscllem  28703  tglng  28896  axlowdimlem6  29412  axlowdimlem16  29422  axlowdimlem17  29423  axlowdim  29426  axeuclidlem  29427  axcontlem2  29430  axcontlem7  29435  axcontlem8  29436  nbusgrvtxm1uvtx  29873  wlk1walk  30106  pthdivtx  30199  pthdadjvtx  30200  crctcshwlkn0lem2  30287  crctcshwlkn0lem4  30289  clwwisshclwws  30493  fusgreg2wsp  30824  nvvcop  31083  nvex  31100  phnv  31303  sheli  31703  cheli  31721  hhssabloilem  31750  choc1  31816  shintcli  31818  chintcli  31820  shsleji  31859  pjini  32188  mayete3i  32217  dmadjop  32377  nlelshi  32549  cnlnadjeui  32566  cnlnssadj  32569  bdopadj  32571  pjimai  32665  stcl  32705  atelch  32833  fcnvgreu  33153  f1od2  33198  fcobijfs  33200  fcobijfs2  33201  uzssico  33263  iundisj2fi  33276  nnindf  33298  eliccioo  33384  gsummptres  33500  cyc3genpm  33600  elrspunidl  33864  0mplrim  34032  psrmonmul  34068  zarcls  34392  ordtrestNEW  34439  xrge0iifcnv  34451  xrge0iifcv  34452  xrge0iifiso  34453  xrge0iifhom  34455  qqhcn  34509  esumval  34564  gsumesum  34577  esumlub  34578  esumcst  34581  esumfsup  34588  issgon  34641  elrnsiga  34644  imambfm  34781  br2base  34788  sxbrsigalem0  34790  dya2iocucvr  34803  sxbrsigalem2  34805  sxbrsigalem5  34807  sxbrsiga  34809  omssubadd  34819  sitmcl  34870  oddpwdc  34873  eulerpartlemelr  34876  eulerpartlemgvv  34895  eulerpartlemgh  34897  eulerpartlemgs2  34899  eulerpartlemn  34900  sseqf  34911  ballotlem2  35008  ballotlemfp1  35011  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemfmpn  35014  ballotlemsup  35024  ballotlemfrceq  35048  signswch  35077  rpsqrtcn  35109  prodfzo03  35119  itgexpif  35122  bnj1533  35369  bnj1137  35512  bnj1286  35536  bnj1408  35553  bnj1417  35558  r1omhf  35622  onvf1odlem4  35711  subfacp1lem5  35771  cvmsi  35852  gonar  35982  goalr  35984  mpst123  36127  mpstrcl  36128  msrrcl  36130  elmsta  36135  msubvrs  36147  elmpps  36160  elmthm  36163  bcprod  36325  dfon2lem4  36371  pprodss4v  36469  ivthALT  36962  neibastop2lem  36987  nnssi2  37082  nnssi3  37083  ttcel2  37128  bj-sngltagi  37734  bj-elid5  37929  bj-fvmptunsn1  38017  bj-smgrpssmgmel  38029  bj-mndsssmgrpel  38031  bj-cmnssmndel  38033  bj-grpssmndel  38035  bj-ablssgrpel  38037  bj-ablsscmnel  38039  bj-vecssmodel  38042  bj-flddrng  38049  bj-rveccvec  38065  bj-rvecabl  38067  taupilemrplb  38080  icorempo  38113  elxp8  38133  sin2h  38372  cos2h  38373  tan2h  38374  poimirlem14  38391  poimirlem26  38403  poimirlem27  38404  poimirlem31  38408  poimirlem32  38409  mblfinlem1  38414  cnambfre  38425  dvtan  38427  itg2addnc  38431  itg2gt0cn  38432  ftc1cnnc  38449  ftc2nc  38459  dvasin  38461  dvacos  38462  cover2  38473  sstotbnd2  38532  heibor1lem  38567  heiborlem10  38578  opidonOLD  38610  exidcl  38634  rngosn3  38682  flddivrng  38757  toycom  39854  osumcllem7N  40843  pexmidlem4N  40854  diaintclN  41939  dibintclN  42048  mapd1o  42529  hdmapevec  42716  dvrelog2  42938  aks6d1c2lem4  43001  sticksstones1  43020  aks6d1c6lem5  43051  redvmptabs  43243  imacrhmcl  43410  prjspvs  43464  prjspeclsp  43466  0prjspnrel  43481  elrfi  43547  elrfirn  43548  elrfirn2  43549  mrefg3  43561  diophin  43625  diophun  43626  eq0rabdioph  43629  eqrabdioph  43630  pellex  43684  rmxycomplete  43766  jm2.23  43845  aomclem2  43904  fglmod  43922  lsmfgcl  43923  lmhmfgima  43933  lmhmfgsplit  43935  isnumbasabl  43955  dgrsub2  43984  itgocn  44013  areaquad  44065  cantnftermord  44169  omabs2  44181  nna1iscard  44393  elmapintrab  44424  corcltrcl  44587  k0004val0  45002  radcnvrat  45146  uzmptshftfval  45178  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  onfrALTlem2  45377  onfrALTlem2VD  45719  uzwo4  45895  mptssid  46078  uzublem  46266  eliccelioc  46359  elicores  46371  sqrlearg  46391  fsumiunss  46413  limcdm0  46456  sumnnodd  46468  fnlimfvre  46510  limsupubuzlem  46548  limsupmnflem  46556  limsupre3uzlem  46571  climuzlem  46579  liminflelimsuplem  46611  cncfshift  46710  cncfperiod  46715  icccncfext  46723  dvnprodlem1  46782  dvnprodlem2  46783  itgsin0pilem1  46786  itgsinexplem1  46790  itgsinexp  46791  ditgeqiooicc  46796  itgsubsticclem  46811  itgioocnicc  46813  itgsbtaddcnst  46818  stoweidlem34  46870  stoweidlem41  46877  stoweidlem51  46887  wallispilem2  46902  stirlinglem11  46920  dirkercncflem2  46940  fourierdlem5  46948  fourierdlem9  46952  fourierdlem17  46960  fourierdlem18  46961  fourierdlem20  46963  fourierdlem39  46982  fourierdlem48  46990  fourierdlem49  46991  fourierdlem62  47004  fourierdlem66  47008  fourierdlem68  47010  fourierdlem72  47014  fourierdlem73  47015  fourierdlem81  47023  fourierdlem83  47025  fourierdlem85  47027  fourierdlem87  47029  fourierdlem88  47030  fourierdlem92  47034  fourierdlem95  47037  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  etransclem24  47094  etransclem35  47105  etransclem37  47107  salexct  47170  salgencntex  47179  sge0resplit  47242  sge0split  47245  meaiuninclem  47316  caratheodorylem1  47362  volicorescl  47389  hoidmv1lelem3  47429  opnvonmbllem2  47469  ovolval2  47480  ovolval3  47483  ovolval4lem1  47485  ovolval4lem2  47486  smfaddlem1  47599  smflimlem2  47608  smfrec  47625  smfdiv  47633  smfsuplem1  47647  smfsuplem3  47649  et-ltneverrefl  47707  wrddrin  47723  wrddun  47725  chndrin  47728  chndun  47730  chnrrin  47733  chnrun  47735  tannpoly  47766  fcores  47963  elfz2nn  48218  rehalfge1  48235  spr0el  48390  nprmdvdsfacm1lem4  48534  nprmdvdsfacm1  48535  ppivalnnnprmge6  48537  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  upgrimpthslem2  48832  stgredgiun  48882  isubgr3stgrlem7  48896  fldhmsubcALTV  49256  fvconst0ci  49825  fvconstdomi  49826  idfullsubc  50095  fulloppf  50097  fthoppf  50098  initopropdlemlem  50173