Theorem sseli 3913

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sselii  3914  sselid  3915  elun1  4106  elun2  4107  elopabran  5467  copsex2ga  5706  2elresin  6537  nfvres  6792  fvco4i  6851  mptrcl  6866  fvmptss  6869  fvmptex  6871  fvmptnf  6879  elfvmptrab1w  6883  elfvmptrab1  6884  fvopab4ndm  6886  fvimacnvi  6911  elpreima  6917  iinpreima  6928  ofrfvalg  7519  ofval  7522  off  7529  nnon  7693  finds  7719  finds2  7721  eqopi  7840  op1steq  7848  dfoprab4  7868  bropopvvv  7901  bropfvvvv  7903  reldmtpos  8021  wfrlem10OLD  8120  smores2  8156  frsuc  8238  nnfiOLD  8946  unifpw  9052  cantnfp1lem1  9366  cantnfp1lem3  9368  r1fin  9462  r1tr  9465  r1ordg  9467  r1ord3g  9468  r1val1  9475  tz9.12lem3  9478  tcrank  9573  cplem1  9578  hta  9586  tskwe  9639  cardprclem  9668  alephfplem3  9793  dfac12r  9833  ackbij1lem16  9922  ackbij2  9930  fin23lem28  10027  fin23lem30  10029  fin23lem31  10030  fin1a2lem6  10092  hsmexlem4  10116  hsmexlem5  10117  hsmexlem6  10118  axdc2lem  10135  axdc3lem2  10138  axcclem  10144  brdom5  10216  brdom4  10217  r1tskina  10469  gruina  10505  grur1a  10506  pinn  10565  0nnq  10611  elpqn  10612  recn  10892  rexr  10952  ltord1  11431  leord1  11432  eqord1  11433  nnre  11910  nncn  11911  nnind  11921  nnnn0  12170  nn0re  12172  nn0cn  12173  nn0xnn0  12239  nnz  12272  nn0z  12273  nnq  12631  qcn  12632  rpre  12667  eliccxr  13096  difreicc  13145  iccshftri  13148  iccshftli  13150  iccdili  13152  icccntri  13154  fzval2  13171  fzelp1  13237  4fvwrd4  13305  elfzo1  13365  ico01fl0  13467  expcllem  13721  expcl2lem  13722  m1expcl2  13732  bcm1k  13957  bcpasc  13963  hashbclem  14092  wrdv  14160  pfxfv0  14333  pfxfvlsw  14336  cshimadifsn  14470  swrds2m  14582  sqrlem5  14886  cau3lem  14994  caubnd  14998  climconst2  15185  o1of2  15250  o1rlimmul  15256  caurcvg  15316  caucvg  15318  binomlem  15469  incexclem  15476  divcnvshft  15495  zprod  15575  fprodge1  15633  risefaccllem  15651  fallfaccllem  15652  bpolydiflem  15692  bpoly4  15697  dvdsflip  15954  divalglem8  16037  sadadd  16102  smumul  16128  isprm3  16316  phimullem  16408  prmdiveq  16415  unbenlem  16537  vdwnnlem1  16624  vdwnnlem3  16626  ramtcl2  16640  prmgaplem4  16683  cshwshashlem1  16725  structcnvcnv  16782  fvsetsid  16797  imasdsval2  17144  mreunirn  17227  mrcfval  17234  mrisval  17256  coapm  17702  tsrss  18222  submnd0  18329  smndex1id  18465  nmzsubg  18708  nmznsg  18711  cntzmhm  18860  symgtrinv  18995  pmtrdifellem4  19002  psgnpmtr  19033  efginvrel2  19248  efginvrel1  19249  efgsp1  19258  efgsres  19259  efgsfo  19260  frgpinv  19285  frgpupf  19294  frgpup1  19296  subcmn  19353  torsubg  19370  dprd2dlem1  19559  dpjidcl  19576  ablfaclem3  19605  acsfn1p  19982  lssacs  20144  cnsubdrglem  20561  rege0subm  20566  rge0srg  20581  zringunit  20600  znrrg  20685  psgnghm  20697  zrhpsgnevpm  20708  evpmodpmf1o  20713  pmtrodpm  20714  phlssphl  20776  frlmsslsp  20913  islinds4  20952  lmimlbs  20953  lbslcic  20958  psrbaglefi  21045  psrbaglefiOLD  21046  psrbagconf1o  21049  mplsubglem  21115  mplneg  21124  ressmpladd  21140  ressmplmul  21141  ressmplvsca  21142  mplmonmul  21147  ply1bascl  21284  mdetralt  21665  mdetunilem7  21675  chfacfpmmulgsum2  21922  tgval2  22014  ordtbas  22251  ordtrestixx  22281  hauslly  22551  kgentop  22601  ptbasin  22636  filunirn  22941  uzrest  22956  elflim  23030  flffval  23048  fclsval  23067  isfcls  23068  fcfval  23092  ustn0  23280  fmucndlem  23351  xmetunirn  23398  mopnval  23499  setsmstopn  23539  tmsval  23542  tngtopn  23720  qtopbaslem  23828  xrtgioo  23875  reperflem  23887  icccmplem1  23891  icopnfhmeo  24012  icccvx  24019  bndth  24027  reparphti  24066  pcoval1  24082  pcoval2  24085  pcoass  24093  pcorevlem  24095  pcorev2  24097  pi1xfrcnv  24126  csscld  24318  cfilfval  24333  caufval  24344  bcthlem1  24393  ivthlem1  24520  ivthlem3  24522  ovolicc2lem3  24588  ovolicc2lem4  24589  vitalilem1  24677  mbflimsup  24735  i1fd  24750  i1f0  24756  i1f1  24759  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  iblmbf  24837  ellimc2  24946  limcres  24955  limcun  24964  dvbsss  24971  perfdvf  24972  dvres2lem  24979  dvaddbr  25007  rolle  25059  cmvth  25060  dvlip  25062  dvlipcn  25063  dvle  25076  lhop1lem  25082  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem2  25096  ftc2  25113  itgparts  25116  itgsubstlem  25117  itgsubst  25118  deg1mul3  25185  coeval  25289  coeeu  25291  dgrval  25294  coef3  25298  coemulc  25321  dgrsub  25338  coecj  25344  dvply2  25351  dvnply  25353  quotval  25357  fta1  25373  plyexmo  25378  aacjcl  25392  taylfval  25423  dvtaylp  25434  abelth  25505  pilem3  25517  cos0pilt1  25593  sinord  25595  recosf1o  25596  resinf1o  25597  tanord1  25598  eff1olem  25609  dvloglem  25708  dvlog  25711  dvlog2lem  25712  advlogexp  25715  logtayl  25720  logtayl2  25722  dvcncxp1  25801  dvcnsqrt  25802  cxpcn3lem  25805  cxpcn3  25806  sqrtcn  25808  loglesqrt  25816  1cubr  25897  acosrecl  25958  efrlim  26024  jensen  26043  lgamgulmlem2  26084  lgamucov2  26093  basellem4  26138  musum  26245  dchrinvcl  26306  dchrghm  26309  dchrinv  26314  dchrsum2  26321  dchrsum  26322  rpvmasumlem  26540  dchrisum0lem2a  26570  pnt  26667  tglng  26811  axlowdimlem6  27218  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  axeuclidlem  27233  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  nbusgrvtxm1uvtx  27675  wlk1walk  27908  pthdivtx  27998  pthdadjvtx  27999  crctcshwlkn0lem2  28077  crctcshwlkn0lem4  28079  clwwisshclwws  28280  fusgreg2wsp  28601  nvvcop  28857  nvex  28874  phnv  29077  sheli  29477  cheli  29495  hhssabloilem  29524  choc1  29590  shintcli  29592  chintcli  29594  shsleji  29633  pjini  29962  mayete3i  29991  dmadjop  30151  nlelshi  30323  cnlnadjeui  30340  cnlnssadj  30343  bdopadj  30345  pjimai  30439  stcl  30479  atelch  30607  fcnvgreu  30912  f1od2  30958  fcobijfs  30960  uzssico  31007  iundisj2fi  31020  nnindf  31035  eliccioo  31107  gsummptres  31214  cyc3genpm  31321  elrspunidl  31508  zarcls  31726  ordtrestNEW  31773  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iifiso  31787  xrge0iifhom  31789  qqhcn  31841  esumval  31914  gsumesum  31927  esumlub  31928  esumcst  31931  esumfsup  31938  issgon  31991  elrnsiga  31994  imambfm  32129  br2base  32136  sxbrsigalem0  32138  dya2iocucvr  32151  sxbrsigalem2  32153  sxbrsigalem5  32155  sxbrsiga  32157  omssubadd  32167  sitmcl  32218  oddpwdc  32221  eulerpartlemelr  32224  eulerpartlemgvv  32243  eulerpartlemgh  32245  eulerpartlemgs2  32247  eulerpartlemn  32248  sseqf  32259  ballotlem2  32355  ballotlemfp1  32358  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfmpn  32361  ballotlemsup  32371  ballotlemfrceq  32395  signswch  32440  rpsqrtcn  32473  prodfzo03  32483  itgexpif  32486  bnj1533  32732  bnj1137  32875  bnj1286  32899  bnj1408  32916  bnj1417  32921  subfacp1lem5  33046  cvmsi  33127  gonar  33257  goalr  33259  mpst123  33402  mpstrcl  33403  msrrcl  33405  elmsta  33410  msubvrs  33422  elmpps  33435  elmthm  33438  bcprod  33610  dfon2lem4  33668  oldf  33968  leftirr  34000  rightirr  34001  lrold  34004  sltlpss  34014  pprodss4v  34113  ivthALT  34451  neibastop2lem  34476  nnssi2  34571  nnssi3  34572  bj-sngltagi  35099  bj-elid5  35267  bj-fvmptunsn1  35355  bj-smgrpssmgmel  35367  bj-mndsssmgrpel  35369  bj-cmnssmndel  35371  bj-grpssmndel  35373  bj-ablssgrpel  35375  bj-ablsscmnel  35377  bj-vecssmodel  35380  bj-flddrng  35387  bj-rveccvec  35403  bj-rvecabl  35405  taupilemrplb  35418  icorempo  35449  elxp8  35469  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem14  35718  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  mblfinlem1  35741  cnambfre  35752  dvtan  35754  itg2addnc  35758  itg2gt0cn  35759  ftc1cnnc  35776  ftc2nc  35786  dvasin  35788  dvacos  35789  cover2  35799  sstotbnd2  35859  heibor1lem  35894  heiborlem10  35905  opidonOLD  35937  exidcl  35961  rngosn3  36009  flddivrng  36084  toycom  36914  osumcllem7N  37903  pexmidlem4N  37914  diaintclN  38999  dibintclN  39108  mapd1o  39589  hdmapevec  39776  dvrelog2  40000  sticksstones1  40030  prjspvs  40370  prjspeclsp  40372  0prjspnrel  40385  elrfi  40432  elrfirn  40433  elrfirn2  40434  mrefg3  40446  diophin  40510  diophun  40511  eq0rabdioph  40514  eqrabdioph  40515  pellex  40573  rmxycomplete  40655  jm2.23  40734  aomclem2  40796  fglmod  40814  lsmfgcl  40815  lmhmfgima  40825  lmhmfgsplit  40827  isnumbasabl  40847  dgrsub2  40876  itgocn  40905  areaquad  40963  elmapintrab  41073  corcltrcl  41236  k0004val0  41653  elscottab  41751  radcnvrat  41821  uzmptshftfval  41853  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  onfrALTlem2  42055  onfrALTlem2VD  42398  uzwo4  42490  mptssid  42674  uzublem  42860  eliccelioc  42949  elicores  42961  sqrlearg  42981  fsumiunss  43006  limcdm0  43049  sumnnodd  43061  fnlimfvre  43105  limsupubuzlem  43143  limsupmnflem  43151  limsupre3uzlem  43166  climuzlem  43174  cncfshift  43305  cncfperiod  43310  icccncfext  43318  dvnprodlem1  43377  dvnprodlem2  43378  itgsin0pilem1  43381  itgsinexplem1  43385  itgsinexp  43386  ditgeqiooicc  43391  itgsubsticclem  43406  itgioocnicc  43408  itgsbtaddcnst  43413  stoweidlem34  43465  stoweidlem41  43472  stoweidlem51  43482  wallispilem2  43497  stirlinglem11  43515  dirkercncflem2  43535  fourierdlem5  43543  fourierdlem9  43547  fourierdlem17  43555  fourierdlem18  43556  fourierdlem20  43558  fourierdlem39  43577  fourierdlem48  43585  fourierdlem49  43586  fourierdlem62  43599  fourierdlem66  43603  fourierdlem68  43605  fourierdlem72  43609  fourierdlem73  43610  fourierdlem81  43618  fourierdlem83  43620  fourierdlem85  43622  fourierdlem87  43624  fourierdlem88  43625  fourierdlem92  43629  fourierdlem95  43632  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  etransclem24  43689  etransclem35  43700  etransclem37  43702  salexct  43763  salgencntex  43772  sge0resplit  43834  sge0split  43837  meaiuninclem  43908  caratheodorylem1  43954  volicorescl  43981  hoidmv1lelem3  44021  opnvonmbllem2  44061  ovolval2  44072  ovolval3  44075  ovolval4lem1  44077  ovolval4lem2  44078  pimiooltgt  44135  sssmf  44161  smfaddlem1  44185  smflimlem2  44194  smfrec  44210  smfdiv  44218  smfsuplem1  44231  smfsuplem3  44233  fcores  44448  spr0el  44822  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  fldhmsubc  45530  fldhmsubcALTV  45548  fvconst0ci  46074  fvconstdomi  46075