Theorem sseli 3931

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  sselii  3932  sselid  3933  elun1  4136  elun2  4137  elopabr  5516  elopabran  5517  elopaelxp  5722  copsex2ga  5764  2elresin  6621  nfvres  6880  fvco4i  6943  mptrcl  6959  fvmptss  6962  fvmptex  6964  fvmptnf  6972  elfvmptrab1w  6977  elfvmptrab1  6978  fvopab4ndm  6980  fvimacnvi  7006  elpreima  7012  iinpreima  7023  ofrfvalg  7640  ofval  7643  off  7650  nnon  7824  finds  7848  finds2  7850  eqopi  7979  op1steq  7987  dfoprab4  8009  bropopvvv  8042  bropfvvvv  8044  reldmtpos  8186  smores2  8296  frsuc  8378  unifpw  9267  cantnfp1lem1  9599  cantnfp1lem3  9601  r1fin  9697  r1tr  9700  r1ordg  9702  r1ord3g  9703  r1val1  9710  tz9.12lem3  9713  tcrank  9808  cplem1  9813  hta  9821  tskwe  9874  cardprclem  9903  alephfplem3  10028  dfac12r  10069  ackbij1lem16  10156  ackbij2  10164  fin23lem28  10262  fin23lem30  10264  fin23lem31  10265  fin1a2lem6  10327  hsmexlem4  10351  hsmexlem5  10352  hsmexlem6  10353  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  brdom5  10451  brdom4  10452  r1tskina  10705  gruina  10741  grur1a  10742  pinn  10801  0nnq  10847  elpqn  10848  recn  11128  rexr  11190  ltord1  11675  leord1  11676  eqord1  11677  nnre  12164  nncn  12165  nnind  12175  nnnn0  12420  nn0re  12422  nn0cn  12423  nn0xnn0  12490  nn0z  12524  uzuzle35  12812  nnq  12887  qcn  12888  rpre  12926  eliccxr  13363  difreicc  13412  iccshftri  13415  iccshftli  13417  iccdili  13419  icccntri  13421  fzval2  13438  fzelp1  13504  4fvwrd4  13576  elfzo1  13640  ico01fl0  13751  expcllem  14007  expcl2lem  14008  m1expcl2  14020  bcm1k  14250  bcpasc  14256  hashbclem  14387  wrdv  14464  pfxfv0  14627  pfxfvlsw  14630  cshimadifsn  14764  swrds2m  14876  01sqrexlem5  15181  cau3lem  15290  caubnd  15294  climconst2  15483  o1of2  15548  o1rlimmul  15554  caurcvg  15612  caucvg  15614  binomlem  15764  incexclem  15771  divcnvshft  15790  zprod  15872  fprodge1  15930  risefaccllem  15948  fallfaccllem  15949  bpolydiflem  15989  bpoly4  15994  dvdsflip  16256  divalglem8  16339  sadadd  16406  smumul  16432  isprm3  16622  phimullem  16718  prmdiveq  16725  unbenlem  16848  vdwnnlem1  16935  vdwnnlem3  16937  ramtcl2  16951  prmgaplem4  16994  cshwshashlem1  17035  structcnvcnv  17092  fvsetsid  17107  imasdsval2  17449  mreunirn  17532  mrcfval  17543  mrisval  17565  coapm  18007  tsrss  18524  chnccat  18561  ex-chn1  18572  submnd0  18700  smndex1id  18848  nmzsubg  19106  nmznsg  19109  cntzmhm  19282  symgtrinv  19413  pmtrdifellem4  19420  psgnpmtr  19451  efginvrel2  19668  efginvrel1  19669  efgsp1  19678  efgsres  19679  efgsfo  19680  frgpinv  19705  frgpupf  19714  frgpup1  19716  subcmn  19778  torsubg  19795  dprd2dlem1  19984  dpjidcl  20001  ablfaclem3  20030  nzrring  20461  lringnzr  20486  fldhmsubc  20730  acsfn1p  20744  lssacs  20930  cnsubdrglem  21385  rege0subm  21390  rge0srg  21405  zringunit  21433  znrrg  21532  psgnghm  21547  zrhpsgnevpm  21558  evpmodpmf1o  21563  pmtrodpm  21564  phlssphl  21626  frlmsslsp  21763  islinds4  21802  lmimlbs  21803  lbslcic  21808  psrbaglefi  21894  psrbagconf1o  21897  mplsubglem  21966  mplneg  21977  ressmpladd  21996  ressmplmul  21997  ressmplvsca  21998  mplmonmul  22003  psdmul  22121  ply1bascl  22156  mdetralt  22564  mdetunilem7  22574  chfacfpmmulgsum2  22821  tgval2  22912  ordtbas  23148  ordtrestixx  23178  hauslly  23448  kgentop  23498  ptbasin  23533  filunirn  23838  uzrest  23853  elflim  23927  flffval  23945  fclsval  23964  isfcls  23965  fcfval  23989  ustn0  24177  fmucndlem  24246  xmetunirn  24293  mopnval  24394  setsmstopn  24434  tmsval  24437  tngtopn  24606  qtopbaslem  24714  xrtgioo  24763  reperflem  24775  icccmplem1  24779  icopnfhmeo  24909  icccvx  24916  bndth  24925  reparphtiOLD  24965  pcoval1  24981  pcoval2  24984  pcoass  24992  pcorevlem  24994  pcorev2  24996  pi1xfrcnv  25025  csscld  25217  cfilfval  25232  caufval  25243  bcthlem1  25292  ivthlem1  25420  ivthlem3  25422  ovolicc2lem3  25488  ovolicc2lem4  25489  vitalilem1  25577  mbflimsup  25635  i1fd  25650  i1f0  25656  i1f1  25659  itg1addlem4  25668  itg1addlem5  25669  iblmbf  25736  ellimc2  25846  limcres  25855  limcun  25864  dvbsss  25871  perfdvf  25872  dvres2lem  25879  dvaddbr  25908  rolle  25962  cmvth  25963  cmvthOLD  25964  dvlip  25966  dvlipcn  25967  dvle  25980  lhop1lem  25986  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc2  26019  itgparts  26022  itgsubstlem  26023  itgsubst  26024  deg1mul3  26089  coeval  26196  coeeu  26198  dgrval  26201  coef3  26205  coemulc  26228  dgrsub  26246  coecj  26252  coecjOLD  26254  dvply2  26262  dvnply  26264  quotval  26268  fta1  26284  plyexmo  26289  aacjcl  26303  taylfval  26334  dvtaylp  26346  abelth  26419  pilem3  26431  cos0pilt1  26509  sinord  26511  recosf1o  26512  resinf1o  26513  tanord1  26514  eff1olem  26525  dvloglem  26625  dvlog  26628  dvlog2lem  26629  advlogexp  26632  logtayl  26637  logtayl2  26639  dvcncxp1  26720  dvcnsqrt  26721  cxpcn3lem  26725  cxpcn3  26726  sqrtcn  26728  loglesqrt  26739  1cubr  26820  acosrecl  26881  efrlim  26947  efrlimOLD  26948  jensen  26967  lgamgulmlem2  27008  lgamucov2  27017  basellem4  27062  musum  27169  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dchrinvcl  27232  dchrghm  27235  dchrinv  27240  dchrsum2  27247  dchrsum  27248  rpvmasumlem  27466  dchrisum0lem2a  27496  pnt  27593  oldf  27845  madeno  27851  oldno  27852  newno  27853  oldmade  27876  leftold  27883  rightold  27884  leftno  27885  rightno  27886  addbdaylem  28025  addbday  28026  negsproplem2  28037  negsid  28049  negsunif  28063  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  precsexlem11  28225  onno  28263  oncutlt  28272  n0no  28331  nnno  28332  nnn0s  28335  nnsgt0  28347  zno  28390  expscllem  28438  tglng  28630  axlowdimlem6  29032  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  axeuclidlem  29047  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  nbusgrvtxm1uvtx  29490  wlk1walk  29724  pthdivtx  29812  pthdadjvtx  29813  crctcshwlkn0lem2  29896  crctcshwlkn0lem4  29898  clwwisshclwws  30102  fusgreg2wsp  30423  nvvcop  30682  nvex  30699  phnv  30902  sheli  31302  cheli  31320  hhssabloilem  31349  choc1  31415  shintcli  31417  chintcli  31419  shsleji  31458  pjini  31787  mayete3i  31816  dmadjop  31976  nlelshi  32148  cnlnadjeui  32165  cnlnssadj  32168  bdopadj  32170  pjimai  32264  stcl  32304  atelch  32432  fcnvgreu  32762  f1od2  32809  fcobijfs  32811  fcobijfs2  32812  uzssico  32875  iundisj2fi  32888  nnindf  32911  eliccioo  33023  gsummptres  33146  cyc3genpm  33246  elrspunidl  33521  psrmonmul  33727  zarcls  34052  ordtrestNEW  34099  xrge0iifcnv  34111  xrge0iifcv  34112  xrge0iifiso  34113  xrge0iifhom  34115  qqhcn  34169  esumval  34224  gsumesum  34237  esumlub  34238  esumcst  34241  esumfsup  34248  issgon  34301  elrnsiga  34304  imambfm  34440  br2base  34447  sxbrsigalem0  34449  dya2iocucvr  34462  sxbrsigalem2  34464  sxbrsigalem5  34466  sxbrsiga  34468  omssubadd  34478  sitmcl  34529  oddpwdc  34532  eulerpartlemelr  34535  eulerpartlemgvv  34554  eulerpartlemgh  34556  eulerpartlemgs2  34558  eulerpartlemn  34559  sseqf  34570  ballotlem2  34667  ballotlemfp1  34670  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemfmpn  34673  ballotlemsup  34683  ballotlemfrceq  34707  signswch  34739  rpsqrtcn  34771  prodfzo03  34781  itgexpif  34784  bnj1533  35028  bnj1137  35171  bnj1286  35195  bnj1408  35212  bnj1417  35217  r1omhf  35283  onvf1odlem4  35322  subfacp1lem5  35400  cvmsi  35481  gonar  35611  goalr  35613  mpst123  35756  mpstrcl  35757  msrrcl  35759  elmsta  35764  msubvrs  35776  elmpps  35789  elmthm  35792  bcprod  35954  dfon2lem4  36000  pprodss4v  36098  ivthALT  36551  neibastop2lem  36576  nnssi2  36671  nnssi3  36672  bj-sngltagi  37230  bj-elid5  37424  bj-fvmptunsn1  37512  bj-smgrpssmgmel  37524  bj-mndsssmgrpel  37526  bj-cmnssmndel  37528  bj-grpssmndel  37530  bj-ablssgrpel  37532  bj-ablsscmnel  37534  bj-vecssmodel  37537  bj-flddrng  37544  bj-rveccvec  37560  bj-rvecabl  37562  taupilemrplb  37575  icorempo  37606  elxp8  37626  sin2h  37861  cos2h  37862  tan2h  37863  poimirlem14  37885  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  mblfinlem1  37908  cnambfre  37919  dvtan  37921  itg2addnc  37925  itg2gt0cn  37926  ftc1cnnc  37943  ftc2nc  37953  dvasin  37955  dvacos  37956  cover2  37966  sstotbnd2  38025  heibor1lem  38060  heiborlem10  38071  opidonOLD  38103  exidcl  38127  rngosn3  38175  flddivrng  38250  toycom  39349  osumcllem7N  40338  pexmidlem4N  40349  diaintclN  41434  dibintclN  41543  mapd1o  42024  hdmapevec  42211  dvrelog2  42434  aks6d1c2lem4  42497  sticksstones1  42516  aks6d1c6lem5  42547  redvmptabs  42730  imacrhmcl  42884  prjspvs  42968  prjspeclsp  42970  0prjspnrel  42985  elrfi  43051  elrfirn  43052  elrfirn2  43053  mrefg3  43065  diophin  43129  diophun  43130  eq0rabdioph  43133  eqrabdioph  43134  pellex  43192  rmxycomplete  43274  jm2.23  43353  aomclem2  43412  fglmod  43430  lsmfgcl  43431  lmhmfgima  43441  lmhmfgsplit  43443  isnumbasabl  43463  dgrsub2  43492  itgocn  43521  areaquad  43573  cantnftermord  43677  omabs2  43689  nna1iscard  43901  elmapintrab  43932  corcltrcl  44095  k0004val0  44510  elscottab  44600  radcnvrat  44670  uzmptshftfval  44702  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  onfrALTlem2  44902  onfrALTlem2VD  45244  uzwo4  45413  mptssid  45599  uzublem  45788  eliccelioc  45881  elicores  45893  sqrlearg  45913  fsumiunss  45935  limcdm0  45978  sumnnodd  45990  fnlimfvre  46032  limsupubuzlem  46070  limsupmnflem  46078  limsupre3uzlem  46093  climuzlem  46101  liminflelimsuplem  46133  cncfshift  46232  cncfperiod  46237  icccncfext  46245  dvnprodlem1  46304  dvnprodlem2  46305  itgsin0pilem1  46308  itgsinexplem1  46312  itgsinexp  46313  ditgeqiooicc  46318  itgsubsticclem  46333  itgioocnicc  46335  itgsbtaddcnst  46340  stoweidlem34  46392  stoweidlem41  46399  stoweidlem51  46409  wallispilem2  46424  stirlinglem11  46442  dirkercncflem2  46462  fourierdlem5  46470  fourierdlem9  46474  fourierdlem17  46482  fourierdlem18  46483  fourierdlem20  46485  fourierdlem39  46504  fourierdlem48  46512  fourierdlem49  46513  fourierdlem62  46526  fourierdlem66  46530  fourierdlem68  46532  fourierdlem72  46536  fourierdlem73  46537  fourierdlem81  46545  fourierdlem83  46547  fourierdlem85  46549  fourierdlem87  46551  fourierdlem88  46552  fourierdlem92  46556  fourierdlem95  46559  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  sqwvfoura  46586  sqwvfourb  46587  fouriersw  46589  etransclem24  46616  etransclem35  46627  etransclem37  46629  salexct  46692  salgencntex  46701  sge0resplit  46764  sge0split  46767  meaiuninclem  46838  caratheodorylem1  46884  volicorescl  46911  hoidmv1lelem3  46951  opnvonmbllem2  46991  ovolval2  47002  ovolval3  47005  ovolval4lem1  47007  ovolval4lem2  47008  sssmf  47096  smfaddlem1  47121  smflimlem2  47130  smfrec  47147  smfdiv  47155  smfsuplem1  47169  smfsuplem3  47171  et-ltneverrefl  47229  natglobalincr  47235  tannpoly  47250  fcores  47427  rehalfge1  47695  spr0el  47842  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbnd  48169  upgrimpthslem2  48268  stgredgiun  48318  isubgr3stgrlem7  48332  fldhmsubcALTV  48693  fvconst0ci  49250  fvconstdomi  49251  idfullsubc  49520  fulloppf  49522  fthoppf  49523  initopropdlemlem  49598