Theorem sseli 3927

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

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

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 2835  df-ss 3916

This theorem is used by:  sselii  3928  sselid  3929  elun1  4128  elun2  4129  elopabr  5539  elopabran  5540  elopaelxp  5745  copsex2ga  5788  imadifssran  6197  2elresin  6653  nfvres  6916  fvco4i  6980  mptrcl  6996  fvmptss  6999  fvmptex  7001  fvmptnf  7009  elfvmptrab1w  7014  elfvmptrab1  7015  fvopab4ndm  7017  fvimacnvi  7044  elpreima  7050  iinpreima  7062  ofrfvalg  7686  ofval  7689  off  7696  nnon  7868  finds  7893  finds2  7895  eqopi  8022  op1steq  8030  dfoprab4  8052  bropopvvv  8087  bropfvvvv  8089  reldmtpos  8232  smores2  8343  frsuc  8426  unifpw  9322  cantnfp1lem1  9657  cantnfp1lem3  9659  r1fin  9755  r1tr  9758  r1ordg  9760  r1ord3g  9761  r1val1  9768  tz9.12lem3  9771  tcrank  9866  elscottab  9881  cplem1  9889  cplem1OLD  9890  hta  9901  htaOLD  9902  tskwe  9955  cardprclem  9984  alephfplem3  10109  dfac12r  10149  ackbij1lem16  10236  ackbij2  10244  fin23lem28  10342  fin23lem30  10344  fin23lem31  10345  fin1a2lem6  10407  hsmexlem4  10431  hsmexlem5  10432  hsmexlem6  10433  axdc2lem  10450  axdc3lem2  10453  axcclem  10459  brdom5  10532  brdom4  10533  r1tskina  10791  gruina  10827  grur1a  10828  pinn  10887  0nnq  10933  elpqn  10934  recn  11214  rexr  11279  ltord1  11764  leord1  11765  eqord1  11766  nnre  12264  nncn  12265  nnind  12275  nnnn0  12535  nn0re  12537  nn0cn  12538  nn0xnn0  12605  nn0z  12639  uzuzle35  12936  nnq  13011  qcn  13012  rpre  13051  eliccxr  13488  difreicc  13537  iccshftri  13540  iccshftli  13542  iccdili  13544  icccntri  13546  fzval2  13564  fzelp1  13631  4fvwrd4  13703  elfzo1  13768  ico01fl0  13880  expcllem  14136  expcl2lem  14137  m1expcl2  14149  bcm1k  14379  bcpasc  14385  hashbclem  14517  wrdv  14594  pfxfv0  14761  pfxfvlsw  14764  cshimadifsn  14900  swrds2m  15012  01sqrexlem5  15333  cau3lem  15442  caubnd  15446  climconst2  15635  o1of2  15700  o1rlimmul  15706  caurcvg  15764  caucvg  15766  binomlem  15918  incexclem  15925  divcnvshft  15944  zprod  16024  fprodge1  16082  risefaccllem  16100  fallfaccllem  16101  bpolydiflem  16140  bpoly4  16145  dvdsflip  16407  divalglem8  16490  sadadd  16557  smumul  16583  isprm3  16773  phimullem  16870  prmdiveq  16877  unbenlem  17000  vdwnnlem1  17087  vdwnnlem3  17089  ramtcl2  17103  prmgaplem4  17146  cshwshashlem1  17187  structcnvcnv  17245  fvsetsid  17260  imasdsval2  17602  mreunirn  17685  mrcfval  17696  mrisval  17718  coapm  18160  tsrss  18677  chnccat  18714  ex-chn1  18725  submnd0OLD  18870  smndex1id  19023  nmzsubg  19288  nmznsg  19291  cntzmhm  19468  symgtrinv  19599  pmtrdifellem4  19606  psgnpmtr  19637  efginvrel2  19854  efginvrel1  19855  efgsp1  19864  efgsres  19865  efgsfo  19866  frgpinv  19891  frgpupf  19900  frgpup1  19902  subcmn  19964  torsubg  19981  dprd2dlem1  20170  dpjidcl  20187  ablfaclem3  20216  nzrring  20676  lringnzr  20703  fldhmsubc  20951  acsfn1p  20965  lssacs  21151  cnsubdrglem  21631  rege0subm  21636  rge0srg  21651  zringunit  21679  znrrg  21778  psgnghm  21793  zrhpsgnevpm  21804  evpmodpmf1o  21809  pmtrodpm  21810  phlssphl  21872  frlmsslsp  22009  islinds4  22048  lmimlbs  22049  lbslcic  22054  psrbaglefi  22141  psrbagconf1o  22144  mplsubglem  22213  mplneg  22224  ressmpladd  22244  ressmplmul  22245  ressmplvsca  22246  mplmonmul  22252  psdmul  22394  ply1bascl  22428  mdetralt  22830  mdetunilem7  22840  chfacfpmmulgsum2  23090  tgval2  23181  ordtbas  23417  ordtrestixx  23447  hauslly  23718  kgentop  23768  ptbasin  23803  filunirn  24108  uzrest  24123  elflim  24197  flffval  24215  fclsval  24234  isfcls  24235  fcfval  24259  ustn0  24447  fmucndlem  24516  xmetunirn  24563  mopnval  24664  setsmstopn  24704  tmsval  24707  tngtopn  24876  qtopbaslem  24984  xrtgioo  25033  reperflem  25045  icccmplem1  25049  icopnfhmeo  25171  icccvx  25178  bndth  25186  pcoval1  25241  pcoval2  25244  pcoass  25252  pcorevlem  25254  pcorev2  25256  pi1xfrcnv  25285  csscld  25477  cfilfval  25492  caufval  25503  bcthlem1  25552  ivthlem1  25679  ivthlem3  25681  ovolicc2lem3  25747  ovolicc2lem4  25748  vitalilem1  25836  mbflimsup  25894  i1fd  25909  i1f0  25915  i1f1  25918  itg1addlem4  25927  itg1addlem5  25928  iblmbf  25995  ellimc2  26104  limcres  26113  limcun  26122  dvbsss  26129  perfdvf  26130  dvres2lem  26137  dvaddbr  26165  rolle  26217  cmvth  26218  dvlip  26220  dvlipcn  26221  dvle  26234  lhop1lem  26240  dvfsumle  26248  dvfsumge  26249  dvfsumabs  26250  dvfsumlem2  26254  ftc2  26271  itgparts  26274  itgsubstlem  26275  itgsubst  26276  deg1mul3  26341  coeval  26449  coeeu  26451  dgrval  26454  coef3  26458  coemulc  26481  dgrsub  26498  coecj  26504  coecjOLD  26506  dvply2  26516  dvnply  26518  quotval  26522  fta1  26538  plyexmo  26545  aacjcl  26563  taylfval  26595  dvtaylp  26606  abelth  26677  pilem3  26689  cos0pilt1  26769  sinord  26771  recosf1o  26772  resinf1o  26773  tanord1  26774  eff1olem  26785  dvloglem  26885  dvlog  26888  dvlog2lem  26889  advlogexp  26892  logtayl  26897  logtayl2  26899  dvcncxp1  26980  dvcnsqrt  26981  cxpcn3lem  26984  cxpcn3  26985  sqrtcn  26987  loglesqrt  26998  1cubr  27079  acosrecl  27140  efrlim  27206  jensen  27225  lgamgulmlem2  27266  lgamucov2  27275  basellem4  27320  musum  27427  mpodvdsmulf1o  27430  fsumdvdsmul  27431  dchrinvcl  27489  dchrghm  27492  dchrinv  27497  dchrsum2  27504  dchrsum  27505  rpvmasumlem  27723  dchrisum0lem2a  27753  pnt  27850  oldf  28102  madeno  28108  oldno  28109  newno  28110  oldmade  28133  leftold  28140  rightold  28141  leftno  28142  rightno  28143  addbdaylem  28282  addbday  28283  negsproplem2  28294  negsid  28306  negsunif  28320  mulsproplem12  28392  mulsproplem13  28393  mulsproplem14  28394  precsexlem11  28482  onno  28520  oncutlt  28529  n0no  28588  nnno  28589  nnn0s  28592  nnsgt0  28604  zno  28647  expscllem  28695  tglng  28888  axlowdimlem6  29404  axlowdimlem16  29414  axlowdimlem17  29415  axlowdim  29418  axeuclidlem  29419  axcontlem2  29422  axcontlem7  29427  axcontlem8  29428  nbusgrvtxm1uvtx  29865  wlk1walk  30098  pthdivtx  30191  pthdadjvtx  30192  crctcshwlkn0lem2  30279  crctcshwlkn0lem4  30281  clwwisshclwws  30485  fusgreg2wsp  30816  nvvcop  31075  nvex  31092  phnv  31295  sheli  31695  cheli  31713  hhssabloilem  31742  choc1  31808  shintcli  31810  chintcli  31812  shsleji  31851  pjini  32180  mayete3i  32209  dmadjop  32369  nlelshi  32541  cnlnadjeui  32558  cnlnssadj  32561  bdopadj  32563  pjimai  32657  stcl  32697  atelch  32825  fcnvgreu  33145  f1od2  33190  fcobijfs  33192  fcobijfs2  33193  uzssico  33255  iundisj2fi  33268  nnindf  33290  eliccioo  33376  gsummptres  33492  cyc3genpm  33592  elrspunidl  33856  0mplrim  34024  psrmonmul  34060  zarcls  34384  ordtrestNEW  34431  xrge0iifcnv  34443  xrge0iifcv  34444  xrge0iifiso  34445  xrge0iifhom  34447  qqhcn  34501  esumval  34556  gsumesum  34569  esumlub  34570  esumcst  34573  esumfsup  34580  issgon  34633  elrnsiga  34636  imambfm  34773  br2base  34780  sxbrsigalem0  34782  dya2iocucvr  34795  sxbrsigalem2  34797  sxbrsigalem5  34799  sxbrsiga  34801  omssubadd  34811  sitmcl  34862  oddpwdc  34865  eulerpartlemelr  34868  eulerpartlemgvv  34887  eulerpartlemgh  34889  eulerpartlemgs2  34891  eulerpartlemn  34892  sseqf  34903  ballotlem2  35000  ballotlemfp1  35003  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemfmpn  35006  ballotlemsup  35016  ballotlemfrceq  35040  signswch  35069  rpsqrtcn  35101  prodfzo03  35111  itgexpif  35114  bnj1533  35361  bnj1137  35504  bnj1286  35528  bnj1408  35545  bnj1417  35550  r1omhf  35614  onvf1odlem4  35703  subfacp1lem5  35763  cvmsi  35844  gonar  35974  goalr  35976  mpst123  36119  mpstrcl  36120  msrrcl  36122  elmsta  36127  msubvrs  36139  elmpps  36152  elmthm  36155  bcprod  36317  dfon2lem4  36363  pprodss4v  36461  ivthALT  36954  neibastop2lem  36979  nnssi2  37074  nnssi3  37075  ttcel2  37120  bj-sngltagi  37726  bj-elid5  37921  bj-fvmptunsn1  38009  bj-smgrpssmgmel  38021  bj-mndsssmgrpel  38023  bj-cmnssmndel  38025  bj-grpssmndel  38027  bj-ablssgrpel  38029  bj-ablsscmnel  38031  bj-vecssmodel  38034  bj-flddrng  38041  bj-rveccvec  38057  bj-rvecabl  38059  taupilemrplb  38072  icorempo  38105  elxp8  38125  sin2h  38364  cos2h  38365  tan2h  38366  poimirlem14  38383  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  mblfinlem1  38406  cnambfre  38417  dvtan  38419  itg2addnc  38423  itg2gt0cn  38424  ftc1cnnc  38441  ftc2nc  38451  dvasin  38453  dvacos  38454  cover2  38465  sstotbnd2  38524  heibor1lem  38559  heiborlem10  38570  opidonOLD  38602  exidcl  38626  rngosn3  38674  flddivrng  38749  toycom  39846  osumcllem7N  40835  pexmidlem4N  40846  diaintclN  41931  dibintclN  42040  mapd1o  42521  hdmapevec  42708  dvrelog2  42930  aks6d1c2lem4  42993  sticksstones1  43012  aks6d1c6lem5  43043  redvmptabs  43235  imacrhmcl  43402  prjspvs  43456  prjspeclsp  43458  0prjspnrel  43473  elrfi  43539  elrfirn  43540  elrfirn2  43541  mrefg3  43553  diophin  43617  diophun  43618  eq0rabdioph  43621  eqrabdioph  43622  pellex  43676  rmxycomplete  43758  jm2.23  43837  aomclem2  43896  fglmod  43914  lsmfgcl  43915  lmhmfgima  43925  lmhmfgsplit  43927  isnumbasabl  43947  dgrsub2  43976  itgocn  44005  areaquad  44057  cantnftermord  44161  omabs2  44173  nna1iscard  44385  elmapintrab  44416  corcltrcl  44579  k0004val0  44994  radcnvrat  45138  uzmptshftfval  45170  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  onfrALTlem2  45369  onfrALTlem2VD  45711  uzwo4  45887  mptssid  46070  uzublem  46258  eliccelioc  46351  elicores  46363  sqrlearg  46383  fsumiunss  46405  limcdm0  46448  sumnnodd  46460  fnlimfvre  46502  limsupubuzlem  46540  limsupmnflem  46548  limsupre3uzlem  46563  climuzlem  46571  liminflelimsuplem  46603  cncfshift  46702  cncfperiod  46707  icccncfext  46715  dvnprodlem1  46774  dvnprodlem2  46775  itgsin0pilem1  46778  itgsinexplem1  46782  itgsinexp  46783  ditgeqiooicc  46788  itgsubsticclem  46803  itgioocnicc  46805  itgsbtaddcnst  46810  stoweidlem34  46862  stoweidlem41  46869  stoweidlem51  46879  wallispilem2  46894  stirlinglem11  46912  dirkercncflem2  46932  fourierdlem5  46940  fourierdlem9  46944  fourierdlem17  46952  fourierdlem18  46953  fourierdlem20  46955  fourierdlem39  46974  fourierdlem48  46982  fourierdlem49  46983  fourierdlem62  46996  fourierdlem66  47000  fourierdlem68  47002  fourierdlem72  47006  fourierdlem73  47007  fourierdlem81  47015  fourierdlem83  47017  fourierdlem85  47019  fourierdlem87  47021  fourierdlem88  47022  fourierdlem92  47026  fourierdlem95  47029  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem24  47086  etransclem35  47097  etransclem37  47099  salexct  47162  salgencntex  47171  sge0resplit  47234  sge0split  47237  meaiuninclem  47308  caratheodorylem1  47354  volicorescl  47381  hoidmv1lelem3  47421  opnvonmbllem2  47461  ovolval2  47472  ovolval3  47475  ovolval4lem1  47477  ovolval4lem2  47478  smfaddlem1  47591  smflimlem2  47600  smfrec  47617  smfdiv  47625  smfsuplem1  47639  smfsuplem3  47641  et-ltneverrefl  47699  wrddrin  47715  wrddun  47717  chndrin  47720  chndun  47722  chnrrin  47725  chnrun  47727  tannpoly  47758  fcores  47955  elfz2nn  48210  rehalfge1  48227  spr0el  48382  nprmdvdsfacm1lem4  48526  nprmdvdsfacm1  48527  ppivalnnnprmge6  48529  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  bgoldbtbnd  48725  upgrimpthslem2  48824  stgredgiun  48874  isubgr3stgrlem7  48888  fldhmsubcALTV  49248  fvconst0ci  49817  fvconstdomi  49818  idfullsubc  50087  fulloppf  50089  fthoppf  50090  initopropdlemlem  50165