Theorem sseli 3925

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3914

This theorem is referenced by:  sselii  3926  sselid  3927  elun1  4127  elun2  4128  elopabr  5495  elopabran  5496  elopaelxp  5701  copsex2ga  5742  2elresin  6597  nfvres  6855  fvco4i  6918  mptrcl  6933  fvmptss  6936  fvmptex  6938  fvmptnf  6946  elfvmptrab1w  6951  elfvmptrab1  6952  fvopab4ndm  6954  fvimacnvi  6980  elpreima  6986  iinpreima  6997  ofrfvalg  7613  ofval  7616  off  7623  nnon  7797  finds  7821  finds2  7823  eqopi  7952  op1steq  7960  dfoprab4  7982  bropopvvv  8015  bropfvvvv  8017  reldmtpos  8159  smores2  8269  frsuc  8351  unifpw  9234  cantnfp1lem1  9563  cantnfp1lem3  9565  r1fin  9661  r1tr  9664  r1ordg  9666  r1ord3g  9667  r1val1  9674  tz9.12lem3  9677  tcrank  9772  cplem1  9777  hta  9785  tskwe  9838  cardprclem  9867  alephfplem3  9992  dfac12r  10033  ackbij1lem16  10120  ackbij2  10128  fin23lem28  10226  fin23lem30  10228  fin23lem31  10229  fin1a2lem6  10291  hsmexlem4  10315  hsmexlem5  10316  hsmexlem6  10317  axdc2lem  10334  axdc3lem2  10337  axcclem  10343  brdom5  10415  brdom4  10416  r1tskina  10668  gruina  10704  grur1a  10705  pinn  10764  0nnq  10810  elpqn  10811  recn  11091  rexr  11153  ltord1  11638  leord1  11639  eqord1  11640  nnre  12127  nncn  12128  nnind  12138  nnnn0  12383  nn0re  12385  nn0cn  12386  nn0xnn0  12453  nnzOLD  12487  nn0z  12488  uzuzle35  12780  nnq  12855  qcn  12856  rpre  12894  eliccxr  13330  difreicc  13379  iccshftri  13382  iccshftli  13384  iccdili  13386  icccntri  13388  fzval2  13405  fzelp1  13471  4fvwrd4  13543  elfzo1  13607  ico01fl0  13718  expcllem  13974  expcl2lem  13975  m1expcl2  13987  bcm1k  14217  bcpasc  14223  hashbclem  14354  wrdv  14431  pfxfv0  14594  pfxfvlsw  14597  cshimadifsn  14731  swrds2m  14843  01sqrexlem5  15148  cau3lem  15257  caubnd  15261  climconst2  15450  o1of2  15515  o1rlimmul  15521  caurcvg  15579  caucvg  15581  binomlem  15731  incexclem  15738  divcnvshft  15757  zprod  15839  fprodge1  15897  risefaccllem  15915  fallfaccllem  15916  bpolydiflem  15956  bpoly4  15961  dvdsflip  16223  divalglem8  16306  sadadd  16373  smumul  16399  isprm3  16589  phimullem  16685  prmdiveq  16692  unbenlem  16815  vdwnnlem1  16902  vdwnnlem3  16904  ramtcl2  16918  prmgaplem4  16961  cshwshashlem1  17002  structcnvcnv  17059  fvsetsid  17074  imasdsval2  17415  mreunirn  17498  mrcfval  17509  mrisval  17531  coapm  17973  tsrss  18490  chnccat  18527  ex-chn1  18538  submnd0  18666  smndex1id  18814  nmzsubg  19072  nmznsg  19075  cntzmhm  19248  symgtrinv  19379  pmtrdifellem4  19386  psgnpmtr  19417  efginvrel2  19634  efginvrel1  19635  efgsp1  19644  efgsres  19645  efgsfo  19646  frgpinv  19671  frgpupf  19680  frgpup1  19682  subcmn  19744  torsubg  19761  dprd2dlem1  19950  dpjidcl  19967  ablfaclem3  19996  nzrring  20426  lringnzr  20451  fldhmsubc  20695  acsfn1p  20709  lssacs  20895  cnsubdrglem  21350  rege0subm  21355  rge0srg  21370  zringunit  21398  znrrg  21497  psgnghm  21512  zrhpsgnevpm  21523  evpmodpmf1o  21528  pmtrodpm  21529  phlssphl  21591  frlmsslsp  21728  islinds4  21767  lmimlbs  21768  lbslcic  21773  psrbaglefi  21858  psrbagconf1o  21861  mplsubglem  21931  mplneg  21942  ressmpladd  21959  ressmplmul  21960  ressmplvsca  21961  mplmonmul  21966  psdmul  22076  ply1bascl  22111  mdetralt  22518  mdetunilem7  22528  chfacfpmmulgsum2  22775  tgval2  22866  ordtbas  23102  ordtrestixx  23132  hauslly  23402  kgentop  23452  ptbasin  23487  filunirn  23792  uzrest  23807  elflim  23881  flffval  23899  fclsval  23918  isfcls  23919  fcfval  23943  ustn0  24131  fmucndlem  24200  xmetunirn  24247  mopnval  24348  setsmstopn  24388  tmsval  24391  tngtopn  24560  qtopbaslem  24668  xrtgioo  24717  reperflem  24729  icccmplem1  24733  icopnfhmeo  24863  icccvx  24870  bndth  24879  reparphtiOLD  24919  pcoval1  24935  pcoval2  24938  pcoass  24946  pcorevlem  24948  pcorev2  24950  pi1xfrcnv  24979  csscld  25171  cfilfval  25186  caufval  25197  bcthlem1  25246  ivthlem1  25374  ivthlem3  25376  ovolicc2lem3  25442  ovolicc2lem4  25443  vitalilem1  25531  mbflimsup  25589  i1fd  25604  i1f0  25610  i1f1  25613  itg1addlem4  25622  itg1addlem5  25623  iblmbf  25690  ellimc2  25800  limcres  25809  limcun  25818  dvbsss  25825  perfdvf  25826  dvres2lem  25833  dvaddbr  25862  rolle  25916  cmvth  25917  cmvthOLD  25918  dvlip  25920  dvlipcn  25921  dvle  25934  lhop1lem  25940  dvfsumle  25948  dvfsumleOLD  25949  dvfsumge  25950  dvfsumabs  25951  dvfsumlem2  25955  dvfsumlem2OLD  25956  ftc2  25973  itgparts  25976  itgsubstlem  25977  itgsubst  25978  deg1mul3  26043  coeval  26150  coeeu  26152  dgrval  26155  coef3  26159  coemulc  26182  dgrsub  26200  coecj  26206  coecjOLD  26208  dvply2  26216  dvnply  26218  quotval  26222  fta1  26238  plyexmo  26243  aacjcl  26257  taylfval  26288  dvtaylp  26300  abelth  26373  pilem3  26385  cos0pilt1  26463  sinord  26465  recosf1o  26466  resinf1o  26467  tanord1  26468  eff1olem  26479  dvloglem  26579  dvlog  26582  dvlog2lem  26583  advlogexp  26586  logtayl  26591  logtayl2  26593  dvcncxp1  26674  dvcnsqrt  26675  cxpcn3lem  26679  cxpcn3  26680  sqrtcn  26682  loglesqrt  26693  1cubr  26774  acosrecl  26835  efrlim  26901  efrlimOLD  26902  jensen  26921  lgamgulmlem2  26962  lgamucov2  26971  basellem4  27016  musum  27123  mpodvdsmulf1o  27126  fsumdvdsmul  27127  dchrinvcl  27186  dchrghm  27189  dchrinv  27194  dchrsum2  27201  dchrsum  27202  rpvmasumlem  27420  dchrisum0lem2a  27450  pnt  27547  oldf  27793  leftirr  27831  rightirr  27832  lrold  27837  newbdayim  27843  sltlpss  27848  addsproplem2  27908  sleadd1  27927  addsuniflem  27939  addsbdaylem  27954  addsbday  27955  negsproplem2  27966  negsid  27978  negsunif  27992  mulsrid  28047  mulsproplem12  28061  mulsproplem13  28062  mulsproplem14  28063  precsexlem9  28148  precsexlem11  28150  onsno  28187  onscutlt  28196  onaddscl  28205  onmulscl  28206  n0sno  28247  nnsno  28248  nnn0s  28251  nnsgt0  28262  zno  28301  expscllem  28348  tglng  28519  axlowdimlem6  28920  axlowdimlem16  28930  axlowdimlem17  28931  axlowdim  28934  axeuclidlem  28935  axcontlem2  28938  axcontlem7  28943  axcontlem8  28944  nbusgrvtxm1uvtx  29378  wlk1walk  29612  pthdivtx  29700  pthdadjvtx  29701  crctcshwlkn0lem2  29784  crctcshwlkn0lem4  29786  clwwisshclwws  29987  fusgreg2wsp  30308  nvvcop  30566  nvex  30583  phnv  30786  sheli  31186  cheli  31204  hhssabloilem  31233  choc1  31299  shintcli  31301  chintcli  31303  shsleji  31342  pjini  31671  mayete3i  31700  dmadjop  31860  nlelshi  32032  cnlnadjeui  32049  cnlnssadj  32052  bdopadj  32054  pjimai  32148  stcl  32188  atelch  32316  fcnvgreu  32647  f1od2  32694  fcobijfs  32696  fcobijfs2  32697  uzssico  32759  iundisj2fi  32771  nnindf  32794  eliccioo  32903  gsummptres  33024  cyc3genpm  33113  elrspunidl  33385  zarcls  33879  ordtrestNEW  33926  xrge0iifcnv  33938  xrge0iifcv  33939  xrge0iifiso  33940  xrge0iifhom  33942  qqhcn  33996  esumval  34051  gsumesum  34064  esumlub  34065  esumcst  34068  esumfsup  34075  issgon  34128  elrnsiga  34131  imambfm  34267  br2base  34274  sxbrsigalem0  34276  dya2iocucvr  34289  sxbrsigalem2  34291  sxbrsigalem5  34293  sxbrsiga  34295  omssubadd  34305  sitmcl  34356  oddpwdc  34359  eulerpartlemelr  34362  eulerpartlemgvv  34381  eulerpartlemgh  34383  eulerpartlemgs2  34385  eulerpartlemn  34386  sseqf  34397  ballotlem2  34494  ballotlemfp1  34497  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemfmpn  34500  ballotlemsup  34510  ballotlemfrceq  34534  signswch  34566  rpsqrtcn  34598  prodfzo03  34608  itgexpif  34611  bnj1533  34856  bnj1137  34999  bnj1286  35023  bnj1408  35040  bnj1417  35045  r1omhf  35109  onvf1odlem4  35142  subfacp1lem5  35220  cvmsi  35301  gonar  35431  goalr  35433  mpst123  35576  mpstrcl  35577  msrrcl  35579  elmsta  35584  msubvrs  35596  elmpps  35609  elmthm  35612  bcprod  35774  dfon2lem4  35820  pprodss4v  35918  ivthALT  36369  neibastop2lem  36394  nnssi2  36489  nnssi3  36490  bj-sngltagi  37016  bj-elid5  37203  bj-fvmptunsn1  37291  bj-smgrpssmgmel  37303  bj-mndsssmgrpel  37305  bj-cmnssmndel  37307  bj-grpssmndel  37309  bj-ablssgrpel  37311  bj-ablsscmnel  37313  bj-vecssmodel  37316  bj-flddrng  37323  bj-rveccvec  37339  bj-rvecabl  37341  taupilemrplb  37354  icorempo  37385  elxp8  37405  sin2h  37650  cos2h  37651  tan2h  37652  poimirlem14  37674  poimirlem26  37686  poimirlem27  37687  poimirlem31  37691  poimirlem32  37692  mblfinlem1  37697  cnambfre  37708  dvtan  37710  itg2addnc  37714  itg2gt0cn  37715  ftc1cnnc  37732  ftc2nc  37742  dvasin  37744  dvacos  37745  cover2  37755  sstotbnd2  37814  heibor1lem  37849  heiborlem10  37860  opidonOLD  37892  exidcl  37916  rngosn3  37964  flddivrng  38039  toycom  39012  osumcllem7N  40001  pexmidlem4N  40012  diaintclN  41097  dibintclN  41206  mapd1o  41687  hdmapevec  41874  dvrelog2  42097  aks6d1c2lem4  42160  sticksstones1  42179  aks6d1c6lem5  42210  redvmptabs  42393  imacrhmcl  42547  prjspvs  42643  prjspeclsp  42645  0prjspnrel  42660  elrfi  42727  elrfirn  42728  elrfirn2  42729  mrefg3  42741  diophin  42805  diophun  42806  eq0rabdioph  42809  eqrabdioph  42810  pellex  42868  rmxycomplete  42950  jm2.23  43029  aomclem2  43088  fglmod  43106  lsmfgcl  43107  lmhmfgima  43117  lmhmfgsplit  43119  isnumbasabl  43139  dgrsub2  43168  itgocn  43197  areaquad  43249  cantnftermord  43353  omabs2  43365  nna1iscard  43578  elmapintrab  43609  corcltrcl  43772  k0004val0  44187  elscottab  44277  radcnvrat  44347  uzmptshftfval  44379  binomcxplemdvsum  44388  binomcxplemnotnn0  44389  onfrALTlem2  44579  onfrALTlem2VD  44921  uzwo4  45090  mptssid  45278  uzublem  45468  eliccelioc  45561  elicores  45573  sqrlearg  45593  fsumiunss  45615  limcdm0  45658  sumnnodd  45670  fnlimfvre  45712  limsupubuzlem  45750  limsupmnflem  45758  limsupre3uzlem  45773  climuzlem  45781  liminflelimsuplem  45813  cncfshift  45912  cncfperiod  45917  icccncfext  45925  dvnprodlem1  45984  dvnprodlem2  45985  itgsin0pilem1  45988  itgsinexplem1  45992  itgsinexp  45993  ditgeqiooicc  45998  itgsubsticclem  46013  itgioocnicc  46015  itgsbtaddcnst  46020  stoweidlem34  46072  stoweidlem41  46079  stoweidlem51  46089  wallispilem2  46104  stirlinglem11  46122  dirkercncflem2  46142  fourierdlem5  46150  fourierdlem9  46154  fourierdlem17  46162  fourierdlem18  46163  fourierdlem20  46165  fourierdlem39  46184  fourierdlem48  46192  fourierdlem49  46193  fourierdlem62  46206  fourierdlem66  46210  fourierdlem68  46212  fourierdlem72  46216  fourierdlem73  46217  fourierdlem81  46225  fourierdlem83  46227  fourierdlem85  46229  fourierdlem87  46231  fourierdlem88  46232  fourierdlem92  46236  fourierdlem95  46239  fourierdlem103  46247  fourierdlem104  46248  fourierdlem112  46256  sqwvfoura  46266  sqwvfourb  46267  fouriersw  46269  etransclem24  46296  etransclem35  46307  etransclem37  46309  salexct  46372  salgencntex  46381  sge0resplit  46444  sge0split  46447  meaiuninclem  46518  caratheodorylem1  46564  volicorescl  46591  hoidmv1lelem3  46631  opnvonmbllem2  46671  ovolval2  46682  ovolval3  46685  ovolval4lem1  46687  ovolval4lem2  46688  pimiooltgt  46748  sssmf  46776  smfaddlem1  46801  smflimlem2  46810  smfrec  46827  smfdiv  46835  smfsuplem1  46849  smfsuplem3  46851  et-ltneverrefl  46909  natglobalincr  46915  tannpoly  46921  fcores  47098  rehalfge1  47366  spr0el  47513  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  bgoldbtbnd  47840  upgrimpthslem2  47939  stgredgiun  47989  isubgr3stgrlem7  48003  fldhmsubcALTV  48364  fvconst0ci  48922  fvconstdomi  48923  idfullsubc  49193  fulloppf  49195  fthoppf  49196  initopropdlemlem  49271