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

This theorem is used by:  sselii  3928  sselid  3929  elun1  4128  elun2  4129  elopabr  5535  elopabran  5536  elopaelxp  5741  copsex2ga  5785  imadifssranOLD  6202  2elresin  6660  nfvres  6923  fvco4i  6987  mptrcl  7003  fvmptss  7006  fvmptex  7008  fvmptnf  7016  elfvmptrab1w  7021  elfvmptrab1  7022  fvopab4ndm  7024  fvimacnvi  7051  elpreima  7057  iinpreima  7069  ofrfvalg  7701  ofval  7704  off  7711  nnon  7883  finds  7908  finds2  7910  eqopi  8037  op1steq  8045  dfoprab4  8066  bropopvvv  8101  bropfvvvv  8103  reldmtpos  8251  smores2  8362  frsuc  8445  unifpw  9344  cantnfp1lem1  9679  cantnfp1lem3  9681  r1fin  9780  r1tr  9783  r1ordg  9785  r1ord3g  9786  r1val1  9793  tz9.12lem3  9796  tcrank  9901  elscottab  9942  cplem1  9950  cplem1OLD  9951  hta  9962  htaOLD  9963  tskwe  10031  cardprclem  10060  alephfplem3  10185  dfac12r  10225  ackbij1lem16  10312  ackbij2  10320  fin23lem28  10418  fin23lem30  10420  fin23lem31  10421  fin1a2lem6  10483  hsmexlem4  10507  hsmexlem5  10508  hsmexlem6  10509  axdc2lem  10526  axdc3lem2  10529  axcclem  10535  brdom5  10608  brdom4  10609  r1tskina  10867  gruina  10903  grur1a  10904  pinn  10963  0nnq  11009  elpqn  11010  recn  11290  rexr  11355  ltord1  11842  leord1  11843  eqord1  11844  nnre  12342  nncn  12343  nnind  12353  nnnn0  12613  nn0re  12615  nn0cn  12616  nn0xnn0  12683  nn0z  12717  uzuzle35  13014  nnq  13089  qcn  13090  rpre  13129  eliccxr  13566  difreicc  13615  iccshftri  13618  iccshftli  13620  iccdili  13622  icccntri  13624  fzval2  13642  fzelp1  13710  4fvwrd4  13782  elfzo1  13847  ico01fl0  13959  expcllem  14215  expcl2lem  14216  m1expcl2  14228  bcm1k  14459  bcpasc  14465  hashbclem  14597  wrdv  14674  pfxfv0  14841  pfxfvlsw  14844  cshimadifsn  14980  swrds2m  15092  01sqrexlem5  15413  cau3lem  15522  caubnd  15526  climconst2  15715  o1of2  15780  o1rlimmul  15786  caurcvg  15844  caucvg  15846  binomlem  15998  incexclem  16005  divcnvshft  16024  zprod  16104  fprodge1  16162  risefaccllem  16180  fallfaccllem  16181  bpolydiflem  16220  bpoly4  16225  dvdsflip  16487  divalglem8  16570  sadadd  16637  smumul  16663  isprm3  16858  phimullem  16956  prmdiveq  16963  unbenlem  17086  vdwnnlem1  17173  vdwnnlem3  17175  ramtcl2  17189  prmgaplem4  17232  cshwshashlem1  17273  structcnvcnv  17331  fvsetsid  17346  imasdsval2  17688  mreunirn  17771  mrcfval  17782  mrisval  17804  coapm  18246  tsrss  18763  chnccat  18800  ex-chn1  18811  submnd0OLD  18957  smndex1id  19110  nmzsubg  19375  nmznsg  19378  cntzmhm  19555  symgtrinv  19686  pmtrdifellem4  19693  psgnpmtr  19724  efginvrel2  19941  efginvrel1  19942  efgsp1  19951  efgsres  19952  efgsfo  19953  frgpinv  19978  frgpupf  19987  frgpup1  19989  subcmn  20051  torsubg  20068  dprd2dlem1  20257  dpjidcl  20274  ablfaclem3  20303  nzrring  20766  lringnzr  20793  fldhmsubc  21042  acsfn1p  21056  lssacs  21242  cnsubdrglem  21724  rege0subm  21729  rge0srg  21744  zringunit  21772  znrrg  21871  psgnghm  21886  zrhpsgnevpm  21897  evpmodpmf1o  21902  pmtrodpm  21903  phlssphl  21965  frlmsslsp  22102  islinds4  22141  lmimlbs  22142  lbslcic  22147  psrbaglefi  22234  psrbagconf1o  22237  mplsubglem  22306  mplneg  22317  ressmpladd  22337  ressmplmul  22338  ressmplvsca  22339  mplmonmul  22345  psdmul  22487  ply1bascl  22521  mdetralt  22923  mdetunilem7  22933  chfacfpmmulgsum2  23183  tgval2  23274  ordtbas  23510  ordtrestixx  23540  hauslly  23811  kgentop  23861  ptbasin  23896  filunirn  24201  uzrest  24216  elflim  24290  flffval  24308  fclsval  24327  isfcls  24328  fcfval  24352  ustn0  24540  fmucndlem  24609  xmetunirn  24656  mopnval  24757  setsmstopn  24797  tmsval  24800  tngtopn  24969  qtopbaslem  25077  xrtgioo  25126  reperflem  25138  icccmplem1  25142  icopnfhmeo  25264  icccvx  25271  bndth  25279  pcoval1  25334  pcoval2  25337  pcoass  25345  pcorevlem  25347  pcorev2  25349  pi1xfrcnv  25378  csscld  25570  cfilfval  25585  caufval  25596  bcthlem1  25645  ivthlem1  25772  ivthlem3  25774  ovolicc2lem3  25840  ovolicc2lem4  25841  vitalilem1  25929  mbflimsup  25987  i1fd  26002  i1f0  26008  i1f1  26011  itg1addlem4  26020  itg1addlem5  26021  iblmbf  26088  ellimc2  26197  limcres  26206  limcun  26215  dvbsss  26222  perfdvf  26223  dvres2lem  26230  dvaddbr  26258  rolle  26310  cmvth  26311  dvlip  26313  dvlipcn  26314  dvle  26327  lhop1lem  26333  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  dvfsumlem2  26347  ftc2  26364  itgparts  26367  itgsubstlem  26368  itgsubst  26369  deg1mul3  26434  coeval  26542  coeeu  26544  dgrval  26547  coef3  26551  coemulc  26574  dgrsub  26591  coecj  26597  dvply2  26607  dvnply  26609  quotval  26613  fta1  26629  plyexmo  26636  aacjcl  26654  taylfval  26686  dvtaylp  26697  abelth  26768  pilem3  26780  cos0pilt1  26860  sinord  26862  recosf1o  26863  resinf1o  26864  tanord1  26865  eff1olem  26876  dvloglem  26976  dvlog  26979  dvlog2lem  26980  advlogexp  26983  logtayl  26988  logtayl2  26990  dvcncxp1  27071  dvcnsqrt  27072  cxpcn3lem  27075  cxpcn3  27076  sqrtcn  27078  loglesqrt  27089  1cubr  27170  acosrecl  27231  efrlim  27297  jensen  27316  lgamgulmlem2  27357  lgamucov2  27366  basellem4  27411  musum  27518  mpodvdsmulf1o  27521  fsumdvdsmul  27522  dchrinvcl  27580  dchrghm  27583  dchrinv  27588  dchrsum2  27595  dchrsum  27596  rpvmasumlem  27814  dchrisum0lem2a  27844  pnt  27941  oldf  28223  madeno  28229  oldno  28230  newno  28231  oldmade  28254  leftold  28261  rightold  28262  leftno  28263  rightno  28264  addbdaylem  28403  addbday  28404  negsproplem2  28415  negsid  28427  negsunif  28441  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  precsexlem11  28603  onno  28641  oncutlt  28650  n0no  28709  nnno  28710  nnn0s  28713  nnsgt0  28725  zno  28768  expscllem  28816  tglng  29009  axlowdimlem6  29525  axlowdimlem16  29535  axlowdimlem17  29536  axlowdim  29539  axeuclidlem  29540  axcontlem2  29543  axcontlem7  29548  axcontlem8  29549  nbusgrvtxm1uvtx  29986  wlk1walk  30219  pthdivtx  30312  pthdadjvtx  30313  crctcshwlkn0lem2  30400  crctcshwlkn0lem4  30402  clwwisshclwws  30606  fusgreg2wsp  30937  nvvcop  31196  nvex  31213  phnv  31416  sheli  31816  cheli  31834  hhssabloilem  31863  choc1  31929  shintcli  31931  chintcli  31933  shsleji  31972  pjini  32301  mayete3i  32330  dmadjop  32490  nlelshi  32662  cnlnadjeui  32679  cnlnssadj  32682  bdopadj  32684  pjimai  32778  stcl  32818  atelch  32946  fcnvgreu  33266  f1od2  33311  fcobijfs  33313  fcobijfs2  33314  uzssico  33376  iundisj2fi  33389  nnindf  33411  eliccioo  33497  gsummptres  33613  cyc3genpm  33713  elrspunidl  33978  0mplrim  34146  psrmonmul  34182  zarcls  34506  ordtrestNEW  34553  xrge0iifcnv  34565  xrge0iifcv  34566  xrge0iifiso  34567  xrge0iifhom  34569  qqhcn  34623  esumval  34678  gsumesum  34691  esumlub  34692  esumcst  34695  esumfsup  34702  issgon  34755  elrnsiga  34758  imambfm  34894  br2base  34901  sxbrsigalem0  34903  dya2iocucvr  34916  sxbrsigalem2  34918  sxbrsigalem5  34920  sxbrsiga  34922  omssubadd  34932  sitmcl  34983  oddpwdc  34986  eulerpartlemelr  34989  eulerpartlemgvv  35008  eulerpartlemgh  35010  eulerpartlemgs2  35012  eulerpartlemn  35013  sseqf  35024  ballotlem2  35121  ballotlemfp1  35124  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemfmpn  35127  ballotlemsup  35137  ballotlemfrceq  35161  signswch  35190  rpsqrtcn  35222  prodfzo03  35232  itgexpif  35235  bnj1533  35482  bnj1137  35625  bnj1286  35649  bnj1408  35666  bnj1417  35671  acwer1prc  35760  onvf1odlem4  35885  subfacp1lem5  35949  cvmsi  36030  gonar  36160  goalr  36162  mpst123  36305  mpstrcl  36306  msrrcl  36308  elmsta  36313  msubvrs  36325  elmpps  36338  elmthm  36341  bcprod  36503  dfon2lem4  36548  pprodss4v  36646  ivthALT  37123  neibastop2lem  37148  nnssi2  37243  nnssi3  37244  ttcel2  37289  bj-sngltagi  37895  bj-elid5  38090  bj-fvmptunsn1  38178  bj-smgrpssmgmel  38190  bj-mndsssmgrpel  38192  bj-cmnssmndel  38194  bj-grpssmndel  38196  bj-ablssgrpel  38198  bj-ablsscmnel  38200  bj-vecssmodel  38203  bj-flddrng  38210  bj-rveccvec  38226  bj-rvecabl  38228  taupilemrplb  38241  icorempo  38274  elxp8  38294  sin2h  38533  cos2h  38534  tan2h  38535  poimirlem14  38552  poimirlem26  38564  poimirlem27  38565  poimirlem31  38569  poimirlem32  38570  mblfinlem1  38575  cnambfre  38586  dvtan  38588  itg2addnc  38592  itg2gt0cn  38593  ftc1cnnc  38610  ftc2nc  38620  dvasin  38622  dvacos  38623  cover2  38649  sstotbnd2  38708  heibor1lem  38743  heiborlem10  38754  opidonOLD  38786  exidcl  38810  rngosn3  38858  flddivrng  38933  toycom  40030  osumcllem7N  41019  pexmidlem4N  41030  diaintclN  42115  dibintclN  42224  mapd1o  42705  hdmapevec  42892  dvrelog2  43114  aks6d1c2lem4  43177  sticksstones1  43196  aks6d1c6lem5  43227  redvmptabs  43411  imacrhmcl  43581  prjspvs  43638  prjspeclsp  43640  0prjspnrel  43663  elrfi  43704  elrfirn  43705  elrfirn2  43706  mrefg3  43718  diophin  43782  diophun  43783  eq0rabdioph  43786  eqrabdioph  43787  pellex  43841  rmxycomplete  43923  jm2.23  44002  aomclem2  44056  fglmod  44074  lsmfgcl  44075  lmhmfgima  44085  lmhmfgsplit  44087  isnumbasabl  44107  dgrsub2  44136  itgocn  44165  areaquad  44217  cantnftermord  44321  omabs2  44333  nna1iscard  44545  elmapintrab  44576  corcltrcl  44738  k0004val0  45153  radcnvrat  45297  uzmptshftfval  45329  binomcxplemdvsum  45338  binomcxplemnotnn0  45339  onfrALTlem2  45528  onfrALTlem2VD  45870  uzwo4  46069  mptssid  46252  uzublem  46439  eliccelioc  46532  elicores  46544  sqrlearg  46564  fsumiunss  46586  limcdm0  46629  sumnnodd  46641  fnlimfvre  46683  limsupubuzlem  46721  limsupmnflem  46729  limsupre3uzlem  46744  climuzlem  46752  liminflelimsuplem  46784  cncfshift  46883  cncfperiod  46888  icccncfext  46896  dvnprodlem1  46955  dvnprodlem2  46956  itgsin0pilem1  46959  itgsinexplem1  46963  itgsinexp  46964  ditgeqiooicc  46969  itgsubsticclem  46984  itgioocnicc  46986  itgsbtaddcnst  46991  stoweidlem34  47043  stoweidlem41  47050  stoweidlem51  47060  wallispilem2  47075  stirlinglem11  47093  dirkercncflem2  47113  fourierdlem5  47121  fourierdlem9  47125  fourierdlem17  47133  fourierdlem18  47134  fourierdlem20  47136  fourierdlem39  47155  fourierdlem48  47163  fourierdlem49  47164  fourierdlem62  47177  fourierdlem66  47181  fourierdlem68  47183  fourierdlem72  47187  fourierdlem73  47188  fourierdlem81  47196  fourierdlem83  47198  fourierdlem85  47200  fourierdlem87  47202  fourierdlem88  47203  fourierdlem92  47207  fourierdlem95  47210  fourierdlem103  47218  fourierdlem104  47219  fourierdlem112  47227  sqwvfoura  47237  sqwvfourb  47238  fouriersw  47240  etransclem24  47267  etransclem35  47278  etransclem37  47280  salexct  47343  salgencntex  47352  sge0resplit  47415  sge0split  47418  meaiuninclem  47489  caratheodorylem1  47535  volicorescl  47562  hoidmv1lelem3  47602  opnvonmbllem2  47642  ovolval2  47653  ovolval3  47656  ovolval4lem1  47658  ovolval4lem2  47659  smfaddlem1  47772  smflimlem2  47781  smfrec  47798  smfdiv  47806  smfsuplem1  47820  smfsuplem3  47822  et-ltneverrefl  47880  wrddrin  47896  wrddun  47898  chndrin  47901  chndun  47903  chnrrin  47906  chnrun  47908  tannpoly  47939  fcores  48136  elfz2nn  48391  rehalfge1  48408  spr0el  48563  nprmdvdsfacm1lem4  48707  nprmdvdsfacm1  48708  ppivalnnnprmge6  48710  bgoldbtbndlem2  48903  bgoldbtbndlem3  48904  bgoldbtbnd  48906  upgrimpthslem2  49005  stgredgiun  49055  isubgr3stgrlem7  49069  fldhmsubcALTV  49429  fvconst0ci  49998  fvconstdomi  49999  idfullsubc  50268  fulloppf  50270  fthoppf  50271  initopropdlemlem  50346