Theorem sseli 3990

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  sselii  3991  sselid  3992  elun1  4191  elun2  4192  elopabr  5570  elopabran  5571  elopaelxp  5777  copsex2ga  5819  2elresin  6689  nfvres  6947  fvco4i  7009  mptrcl  7024  fvmptss  7027  fvmptex  7029  fvmptnf  7037  elfvmptrab1w  7042  elfvmptrab1  7043  fvopab4ndm  7045  fvimacnvi  7071  elpreima  7077  iinpreima  7088  ofrfvalg  7704  ofval  7707  off  7714  nnon  7892  finds  7918  finds2  7920  eqopi  8048  op1steq  8056  dfoprab4  8078  bropopvvv  8113  bropfvvvv  8115  reldmtpos  8257  wfrlem10OLD  8356  smores2  8392  frsuc  8475  unifpw  9392  cantnfp1lem1  9715  cantnfp1lem3  9717  r1fin  9810  r1tr  9813  r1ordg  9815  r1ord3g  9816  r1val1  9823  tz9.12lem3  9826  tcrank  9921  cplem1  9926  hta  9934  tskwe  9987  cardprclem  10016  alephfplem3  10143  dfac12r  10184  ackbij1lem16  10271  ackbij2  10279  fin23lem28  10377  fin23lem30  10379  fin23lem31  10380  fin1a2lem6  10442  hsmexlem4  10466  hsmexlem5  10467  hsmexlem6  10468  axdc2lem  10485  axdc3lem2  10488  axcclem  10494  brdom5  10566  brdom4  10567  r1tskina  10819  gruina  10855  grur1a  10856  pinn  10915  0nnq  10961  elpqn  10962  recn  11242  rexr  11304  ltord1  11786  leord1  11787  eqord1  11788  nnre  12270  nncn  12271  nnind  12281  nnnn0  12530  nn0re  12532  nn0cn  12533  nn0xnn0  12600  nnzOLD  12634  nn0z  12635  nnq  13001  qcn  13002  rpre  13040  eliccxr  13471  difreicc  13520  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  fzval2  13546  fzelp1  13612  4fvwrd4  13684  elfzo1  13748  ico01fl0  13855  expcllem  14109  expcl2lem  14110  m1expcl2  14122  bcm1k  14350  bcpasc  14356  hashbclem  14487  wrdv  14563  pfxfv0  14726  pfxfvlsw  14729  cshimadifsn  14864  swrds2m  14976  01sqrexlem5  15281  cau3lem  15389  caubnd  15393  climconst2  15580  o1of2  15645  o1rlimmul  15651  caurcvg  15709  caucvg  15711  binomlem  15861  incexclem  15868  divcnvshft  15887  zprod  15969  fprodge1  16027  risefaccllem  16045  fallfaccllem  16046  bpolydiflem  16086  bpoly4  16091  dvdsflip  16350  divalglem8  16433  sadadd  16500  smumul  16526  isprm3  16716  phimullem  16812  prmdiveq  16819  unbenlem  16941  vdwnnlem1  17028  vdwnnlem3  17030  ramtcl2  17044  prmgaplem4  17087  cshwshashlem1  17129  structcnvcnv  17186  fvsetsid  17201  imasdsval2  17562  mreunirn  17645  mrcfval  17652  mrisval  17674  coapm  18124  tsrss  18646  submnd0  18788  smndex1id  18936  nmzsubg  19195  nmznsg  19198  cntzmhm  19371  symgtrinv  19504  pmtrdifellem4  19511  psgnpmtr  19542  efginvrel2  19759  efginvrel1  19760  efgsp1  19769  efgsres  19770  efgsfo  19771  frgpinv  19796  frgpupf  19805  frgpup1  19807  subcmn  19869  torsubg  19886  dprd2dlem1  20075  dpjidcl  20092  ablfaclem3  20121  nzrring  20532  lringnzr  20557  fldhmsubc  20802  acsfn1p  20816  lssacs  20982  cnsubdrglem  21453  rege0subm  21458  rge0srg  21473  zringunit  21494  znrrg  21601  psgnghm  21615  zrhpsgnevpm  21626  evpmodpmf1o  21631  pmtrodpm  21632  phlssphl  21694  frlmsslsp  21833  islinds4  21872  lmimlbs  21873  lbslcic  21878  psrbaglefi  21963  psrbagconf1o  21966  mplsubglem  22036  mplneg  22047  ressmpladd  22064  ressmplmul  22065  ressmplvsca  22066  mplmonmul  22071  psdmul  22187  ply1bascl  22220  mdetralt  22629  mdetunilem7  22639  chfacfpmmulgsum2  22886  tgval2  22978  ordtbas  23215  ordtrestixx  23245  hauslly  23515  kgentop  23565  ptbasin  23600  filunirn  23905  uzrest  23920  elflim  23994  flffval  24012  fclsval  24031  isfcls  24032  fcfval  24056  ustn0  24244  fmucndlem  24315  xmetunirn  24362  mopnval  24463  setsmstopn  24505  tmsval  24508  tngtopn  24686  qtopbaslem  24794  xrtgioo  24841  reperflem  24853  icccmplem1  24857  icopnfhmeo  24987  icccvx  24994  bndth  25003  reparphtiOLD  25043  pcoval1  25059  pcoval2  25062  pcoass  25070  pcorevlem  25072  pcorev2  25074  pi1xfrcnv  25103  csscld  25296  cfilfval  25311  caufval  25322  bcthlem1  25371  ivthlem1  25499  ivthlem3  25501  ovolicc2lem3  25567  ovolicc2lem4  25568  vitalilem1  25656  mbflimsup  25714  i1fd  25729  i1f0  25735  i1f1  25738  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  iblmbf  25816  ellimc2  25926  limcres  25935  limcun  25944  dvbsss  25951  perfdvf  25952  dvres2lem  25959  dvaddbr  25988  rolle  26042  cmvth  26043  cmvthOLD  26044  dvlip  26046  dvlipcn  26047  dvle  26060  lhop1lem  26066  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc2  26099  itgparts  26102  itgsubstlem  26103  itgsubst  26104  deg1mul3  26169  coeval  26276  coeeu  26278  dgrval  26281  coef3  26285  coemulc  26308  dgrsub  26326  coecj  26332  coecjOLD  26334  dvply2  26342  dvnply  26344  quotval  26348  fta1  26364  plyexmo  26369  aacjcl  26383  taylfval  26414  dvtaylp  26426  abelth  26499  pilem3  26511  cos0pilt1  26588  sinord  26590  recosf1o  26591  resinf1o  26592  tanord1  26593  eff1olem  26604  dvloglem  26704  dvlog  26707  dvlog2lem  26708  advlogexp  26711  logtayl  26716  logtayl2  26718  dvcncxp1  26799  dvcnsqrt  26800  cxpcn3lem  26804  cxpcn3  26805  sqrtcn  26807  loglesqrt  26818  1cubr  26899  acosrecl  26960  efrlim  27026  efrlimOLD  27027  jensen  27046  lgamgulmlem2  27087  lgamucov2  27096  basellem4  27141  musum  27248  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dchrinvcl  27311  dchrghm  27314  dchrinv  27319  dchrsum2  27326  dchrsum  27327  rpvmasumlem  27545  dchrisum0lem2a  27575  pnt  27672  oldf  27910  leftirr  27943  rightirr  27944  lrold  27949  sltlpss  27959  addsproplem2  28017  sleadd1  28036  addsuniflem  28048  addsbdaylem  28063  addsbday  28064  negsproplem2  28075  negsid  28087  negsunif  28101  mulsrid  28153  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  precsexlem9  28253  precsexlem11  28255  onsno  28292  onaddscl  28300  onmulscl  28301  n0sno  28342  nnsno  28343  nnn0s  28346  nnsgt0  28356  zno  28382  tglng  28568  axlowdimlem6  28976  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  axeuclidlem  28991  axcontlem2  28994  axcontlem7  28999  axcontlem8  29000  nbusgrvtxm1uvtx  29436  wlk1walk  29671  pthdivtx  29761  pthdadjvtx  29762  crctcshwlkn0lem2  29840  crctcshwlkn0lem4  29842  clwwisshclwws  30043  fusgreg2wsp  30364  nvvcop  30622  nvex  30639  phnv  30842  sheli  31242  cheli  31260  hhssabloilem  31289  choc1  31355  shintcli  31357  chintcli  31359  shsleji  31398  pjini  31727  mayete3i  31756  dmadjop  31916  nlelshi  32088  cnlnadjeui  32105  cnlnssadj  32108  bdopadj  32110  pjimai  32204  stcl  32244  atelch  32372  fcnvgreu  32689  f1od2  32738  fcobijfs  32740  uzssico  32792  iundisj2fi  32804  nnindf  32825  eliccioo  32897  gsummptres  33037  cyc3genpm  33154  elrspunidl  33435  zarcls  33834  ordtrestNEW  33881  xrge0iifcnv  33893  xrge0iifcv  33894  xrge0iifiso  33895  xrge0iifhom  33897  qqhcn  33953  esumval  34026  gsumesum  34039  esumlub  34040  esumcst  34043  esumfsup  34050  issgon  34103  elrnsiga  34106  imambfm  34243  br2base  34250  sxbrsigalem0  34252  dya2iocucvr  34265  sxbrsigalem2  34267  sxbrsigalem5  34269  sxbrsiga  34271  omssubadd  34281  sitmcl  34332  oddpwdc  34335  eulerpartlemelr  34338  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemgs2  34361  eulerpartlemn  34362  sseqf  34373  ballotlem2  34469  ballotlemfp1  34472  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemfmpn  34475  ballotlemsup  34485  ballotlemfrceq  34509  signswch  34554  rpsqrtcn  34586  prodfzo03  34596  itgexpif  34599  bnj1533  34844  bnj1137  34987  bnj1286  35011  bnj1408  35028  bnj1417  35033  subfacp1lem5  35168  cvmsi  35249  gonar  35379  goalr  35381  mpst123  35524  mpstrcl  35525  msrrcl  35527  elmsta  35532  msubvrs  35544  elmpps  35557  elmthm  35560  bcprod  35717  dfon2lem4  35767  pprodss4v  35865  ivthALT  36317  neibastop2lem  36342  nnssi2  36437  nnssi3  36438  bj-sngltagi  36964  bj-elid5  37151  bj-fvmptunsn1  37239  bj-smgrpssmgmel  37251  bj-mndsssmgrpel  37253  bj-cmnssmndel  37255  bj-grpssmndel  37257  bj-ablssgrpel  37259  bj-ablsscmnel  37261  bj-vecssmodel  37264  bj-flddrng  37271  bj-rveccvec  37287  bj-rvecabl  37289  taupilemrplb  37302  icorempo  37333  elxp8  37353  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem14  37620  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  mblfinlem1  37643  cnambfre  37654  dvtan  37656  itg2addnc  37660  itg2gt0cn  37661  ftc1cnnc  37678  ftc2nc  37688  dvasin  37690  dvacos  37691  cover2  37701  sstotbnd2  37760  heibor1lem  37795  heiborlem10  37806  opidonOLD  37838  exidcl  37862  rngosn3  37910  flddivrng  37985  toycom  38954  osumcllem7N  39944  pexmidlem4N  39955  diaintclN  41040  dibintclN  41149  mapd1o  41630  hdmapevec  41817  dvrelog2  42045  aks6d1c2lem4  42108  sticksstones1  42127  aks6d1c6lem5  42158  redvmptabs  42368  imacrhmcl  42500  prjspvs  42596  prjspeclsp  42598  0prjspnrel  42613  elrfi  42681  elrfirn  42682  elrfirn2  42683  mrefg3  42695  diophin  42759  diophun  42760  eq0rabdioph  42763  eqrabdioph  42764  pellex  42822  rmxycomplete  42905  jm2.23  42984  aomclem2  43043  fglmod  43061  lsmfgcl  43062  lmhmfgima  43072  lmhmfgsplit  43074  isnumbasabl  43094  dgrsub2  43123  itgocn  43152  areaquad  43204  cantnftermord  43309  omabs2  43321  nna1iscard  43534  elmapintrab  43565  corcltrcl  43728  k0004val0  44143  elscottab  44239  radcnvrat  44309  uzmptshftfval  44341  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  onfrALTlem2  44543  onfrALTlem2VD  44886  uzwo4  44992  mptssid  45184  uzublem  45379  eliccelioc  45473  elicores  45485  sqrlearg  45505  fsumiunss  45530  limcdm0  45573  sumnnodd  45585  fnlimfvre  45629  limsupubuzlem  45667  limsupmnflem  45675  limsupre3uzlem  45690  climuzlem  45698  cncfshift  45829  cncfperiod  45834  icccncfext  45842  dvnprodlem1  45901  dvnprodlem2  45902  itgsin0pilem1  45905  itgsinexplem1  45909  itgsinexp  45910  ditgeqiooicc  45915  itgsubsticclem  45930  itgioocnicc  45932  itgsbtaddcnst  45937  stoweidlem34  45989  stoweidlem41  45996  stoweidlem51  46006  wallispilem2  46021  stirlinglem11  46039  dirkercncflem2  46059  fourierdlem5  46067  fourierdlem9  46071  fourierdlem17  46079  fourierdlem18  46080  fourierdlem20  46082  fourierdlem39  46101  fourierdlem48  46109  fourierdlem49  46110  fourierdlem62  46123  fourierdlem66  46127  fourierdlem68  46129  fourierdlem72  46133  fourierdlem73  46134  fourierdlem81  46142  fourierdlem83  46144  fourierdlem85  46146  fourierdlem87  46148  fourierdlem88  46149  fourierdlem92  46153  fourierdlem95  46156  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  etransclem24  46213  etransclem35  46224  etransclem37  46226  salexct  46289  salgencntex  46298  sge0resplit  46361  sge0split  46364  meaiuninclem  46435  caratheodorylem1  46481  volicorescl  46508  hoidmv1lelem3  46548  opnvonmbllem2  46588  ovolval2  46599  ovolval3  46602  ovolval4lem1  46604  ovolval4lem2  46605  pimiooltgt  46665  sssmf  46693  smfaddlem1  46718  smflimlem2  46727  smfrec  46744  smfdiv  46752  smfsuplem1  46766  smfsuplem3  46768  et-ltneverrefl  46826  natglobalincr  46830  fcores  47016  spr0el  47406  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  stgredgiun  47860  isubgr3stgrlem7  47874  fldhmsubcALTV  48176  fvconst0ci  48688  fvconstdomi  48689