Theorem sseli 3905

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3897

This theorem is used by:  sselii  3906  sselid  3907  elun1  4179  elun2  4180  elopabr  5535  elopabran  5536  elopaelxp  5742  copsex2ga  5786  imadifssranOLD  6205  2elresin  6665  nfvres  6928  fvco4i  6992  mptrcl  7008  fvmptss  7011  fvmptex  7013  fvmptnf  7021  elfvmptrab1w  7026  elfvmptrab1  7027  fvopab4ndm  7029  fvimacnvi  7056  elpreima  7062  iinpreima  7074  ofrfvalg  7705  ofval  7708  off  7715  nnon  7887  finds  7912  finds2  7914  eqopi  8041  op1steq  8049  dfoprab4  8071  bropopvvv  8106  bropfvvvv  8108  f1od2  8115  reldmtpos  8259  smores2  8370  frsuc  8453  unifpw  9352  cantnfp1lem1  9686  cantnfp1lem3  9688  r1fin  9787  r1tr  9790  r1ordg  9792  r1ord3g  9793  r1val1  9800  tz9.12lem3  9803  tcrank  9908  elscottab  9949  cplem1  9957  cplem1OLD  9958  hta  9969  htaOLD  9970  tskwe  10038  cardprclem  10067  alephfplem3  10192  dfac12r  10232  ackbij1lem16  10319  ackbij2  10327  fin23lem28  10425  fin23lem30  10427  fin23lem31  10428  fin1a2lem6  10490  hsmexlem4  10514  hsmexlem5  10515  hsmexlem6  10516  axdc2lem  10533  axdc3lem2  10536  axcclem  10542  brdom5  10615  brdom4  10616  r1tskina  10874  gruina  10910  grur1a  10911  pinn  10970  0nnq  11016  elpqn  11017  recn  11297  rexr  11362  ltord1  11849  leord1  11850  eqord1  11851  nnre  12349  nncn  12350  nnind  12360  nnnn0  12620  nn0re  12622  nn0cn  12623  nn0xnn0  12690  nn0z  12724  uzuzle35  13021  nnq  13096  qcn  13097  rpre  13136  eliccxr  13573  difreicc  13622  iccshftri  13625  iccshftli  13627  iccdili  13629  icccntri  13631  fzval2  13649  fzelp1  13717  4fvwrd4  13789  elfzo1  13854  ico01fl0  13966  expcllem  14222  expcl2lem  14223  m1expcl2  14235  bcm1k  14466  bcpasc  14472  hashbclem  14604  wrdv  14681  pfxfv0  14849  pfxfvlsw  14852  cshimadifsn  14988  swrds2m  15101  01sqrexlem5  15422  cau3lem  15531  caubnd  15535  climconst2  15724  o1of2  15789  o1rlimmul  15795  caurcvg  15853  caucvg  15855  binomlem  16007  incexclem  16014  divcnvshft  16033  zprod  16113  fprodge1  16171  risefaccllem  16189  fallfaccllem  16190  bpolydiflem  16229  bpoly4  16234  dvdsflip  16496  divalglem8  16579  sadadd  16646  smumul  16672  isprm3  16867  phimullem  16965  prmdiveq  16972  unbenlem  17095  vdwnnlem1  17182  vdwnnlem3  17184  ramtcl2  17198  prmgaplem4  17241  cshwshashlem1  17282  structcnvcnv  17340  fvsetsid  17355  imasdsval2  17697  mreunirn  17780  mrcfval  17791  mrisval  17813  coapm  18255  tsrss  18772  chnccat  18809  ex-chn1  18820  submnd0OLD  18966  smndex1id  19119  nmzsubg  19384  nmznsg  19387  cntzmhm  19564  symgtrinv  19695  pmtrdifellem4  19702  psgnpmtr  19733  efginvrel2  19950  efginvrel1  19951  efgsp1  19960  efgsres  19961  efgsfo  19962  frgpinv  19987  frgpupf  19996  frgpup1  19998  subcmn  20060  torsubg  20077  dprd2dlem1  20266  dpjidcl  20283  ablfaclem3  20312  nzrring  20775  lringnzr  20802  fldhmsubc  21051  acsfn1p  21065  lssacs  21251  cnsubdrglem  21733  rege0subm  21738  rge0srg  21753  zringunit  21781  znrrg  21880  psgnghm  21895  zrhpsgnevpm  21906  evpmodpmf1o  21911  pmtrodpm  21912  phlssphl  21974  frlmsslsp  22111  islinds4  22150  lmimlbs  22151  lbslcic  22156  psrbaglefi  22243  psrbagconf1o  22246  mplsubglem  22315  mplneg  22326  ressmpladd  22346  ressmplmul  22347  ressmplvsca  22348  mplmonmul  22354  psdmul  22496  ply1bascl  22530  mdetralt  22932  mdetunilem7  22942  chfacfpmmulgsum2  23192  tgval2  23283  ordtbas  23519  ordtrestixx  23549  hauslly  23820  kgentop  23870  ptbasin  23905  filunirn  24210  uzrest  24225  elflim  24299  flffval  24317  fclsval  24336  isfcls  24337  fcfval  24361  ustn0  24549  fmucndlem  24618  xmetunirn  24665  mopnval  24766  setsmstopn  24806  tmsval  24809  tngtopn  24978  qtopbaslem  25086  xrtgioo  25135  reperflem  25147  icccmplem1  25151  icopnfhmeo  25273  icccvx  25280  bndth  25288  pcoval1  25343  pcoval2  25346  pcoass  25354  pcorevlem  25356  pcorev2  25358  pi1xfrcnv  25387  csscld  25579  cfilfval  25594  caufval  25605  bcthlem1  25654  ivthlem1  25781  ivthlem3  25783  ovolicc2lem3  25849  ovolicc2lem4  25850  vitalilem1  25938  mbflimsup  25996  i1fd  26011  i1f0  26017  i1f1  26020  itg1addlem4  26029  itg1addlem5  26030  iblmbf  26097  ellimc2  26206  limcres  26215  limcun  26224  dvbsss  26231  perfdvf  26232  dvres2lem  26239  dvaddbr  26267  rolle  26319  cmvth  26320  dvlip  26322  dvlipcn  26323  dvle  26336  lhop1lem  26342  dvfsumle  26350  dvfsumge  26351  dvfsumabs  26352  dvfsumlem2  26356  ftc2  26373  itgparts  26376  itgsubstlem  26377  itgsubst  26378  deg1mul3  26443  coeval  26551  coeeu  26553  dgrval  26556  coef3  26560  coemulc  26583  dgrsub  26600  coecj  26606  dvply2  26616  dvnply  26618  quotval  26622  fta1  26638  plyexmo  26645  aacjcl  26663  taylfval  26695  dvtaylp  26706  abelth  26777  pilem3  26789  cos0pilt1  26869  sinord  26871  recosf1o  26872  resinf1o  26873  tanord1  26874  eff1olem  26885  dvloglem  26985  dvlog  26988  dvlog2lem  26989  advlogexp  26992  logtayl  26997  logtayl2  26999  dvcncxp1  27080  dvcnsqrt  27081  cxpcn3lem  27084  cxpcn3  27085  sqrtcn  27087  loglesqrt  27098  1cubr  27179  acosrecl  27240  efrlim  27306  jensen  27325  lgamgulmlem2  27366  lgamucov2  27375  basellem4  27420  musum  27527  mpodvdsmulf1o  27530  fsumdvdsmul  27531  dchrinvcl  27589  dchrghm  27592  dchrinv  27597  dchrsum2  27604  dchrsum  27605  rpvmasumlem  27823  dchrisum0lem2a  27853  pnt  27950  oldf  28232  madeno  28238  oldno  28239  newno  28240  oldmade  28263  leftold  28270  rightold  28271  leftno  28272  rightno  28273  addbdaylem  28412  addbday  28413  negsproplem2  28424  negsid  28436  negsunif  28450  mulsproplem12  28522  mulsproplem13  28523  mulsproplem14  28524  precsexlem11  28612  onno  28650  oncutlt  28659  n0no  28718  nnno  28719  nnn0s  28722  nnsgt0  28734  zno  28777  expscllem  28825  tglng  29018  axlowdimlem6  29534  axlowdimlem16  29544  axlowdimlem17  29545  axlowdim  29548  axeuclidlem  29549  axcontlem2  29552  axcontlem7  29557  axcontlem8  29558  nbusgrvtxm1uvtx  29995  wlk1walk  30228  pthdivtx  30321  pthdadjvtx  30322  crctcshwlkn0lem2  30409  crctcshwlkn0lem4  30411  clwwisshclwws  30615  fusgreg2wsp  30946  nvvcop  31205  nvex  31222  phnv  31425  sheli  31825  cheli  31843  hhssabloilem  31872  choc1  31938  shintcli  31940  chintcli  31942  shsleji  31981  pjini  32310  mayete3i  32339  dmadjop  32499  nlelshi  32671  cnlnadjeui  32688  cnlnssadj  32691  bdopadj  32693  pjimai  32787  stcl  32827  atelch  32955  fcnvgreu  33317  fcobijfs  33363  fcobijfs2  33364  uzssico  33426  iundisj2fi  33439  nnindf  33461  eliccioo  33547  gsummptres  33663  cyc3genpm  33763  elrspunidl  34028  0mplrim  34196  psrmonmul  34232  zarcls  34556  ordtrestNEW  34603  xrge0iifcnv  34615  xrge0iifcv  34616  xrge0iifiso  34617  xrge0iifhom  34619  qqhcn  34673  esumval  34728  gsumesum  34741  esumlub  34742  esumcst  34745  esumfsup  34752  issgon  34805  elrnsiga  34808  imambfm  34944  br2base  34951  sxbrsigalem0  34953  dya2iocucvr  34966  sxbrsigalem2  34968  sxbrsigalem5  34970  sxbrsiga  34972  omssubadd  34982  sitmcl  35033  oddpwdc  35036  eulerpartlemelr  35039  eulerpartlemgvv  35058  eulerpartlemgh  35060  eulerpartlemgs2  35062  eulerpartlemn  35063  sseqf  35074  ballotlem2  35171  ballotlemfp1  35174  ballotlemfc0  35175  ballotlemfcc  35176  ballotlemfmpn  35177  ballotlemsup  35187  ballotlemfrceq  35211  signswch  35240  rpsqrtcn  35272  prodfzo03  35282  itgexpif  35285  bnj1533  35532  bnj1137  35675  bnj1286  35699  bnj1408  35716  bnj1417  35721  acwer1prc  35828  onvf1odlem4  35985  subfacp1lem5  36067  cvmsi  36148  gonar  36278  goalr  36280  mpst123  36423  mpstrcl  36424  msrrcl  36426  elmsta  36431  msubvrs  36443  elmpps  36456  elmthm  36459  bcprod  36627  dfon2lem1  36669  dfon2lem4  36672  pprodss4v  36770  ivthALT  37247  neibastop2lem  37272  nnssi2  37367  nnssi3  37368  ttcel2  37413  bj-sngltagi  38019  bj-elid5  38227  bj-fvmptunsn1  38315  bj-smgrpssmgmel  38327  bj-mndsssmgrpel  38329  bj-cmnssmndel  38331  bj-grpssmndel  38333  bj-ablssgrpel  38335  bj-ablsscmnel  38337  bj-vecssmodel  38340  bj-flddrng  38347  bj-rveccvec  38363  bj-rvecabl  38365  taupilemrplb  38378  icorempo  38411  elxp8  38431  sin2h  38670  cos2h  38671  tan2h  38672  poimirlem14  38689  poimirlem26  38701  poimirlem27  38702  poimirlem31  38706  poimirlem32  38707  mblfinlem1  38712  cnambfre  38723  dvtan  38725  itg2addnc  38729  itg2gt0cn  38730  ftc1cnnc  38747  ftc2nc  38757  dvasin  38759  dvacos  38760  cover2  38786  sstotbnd2  38845  heibor1lem  38880  heiborlem10  38891  opidonOLD  38923  exidcl  38947  rngosn3  38995  flddivrng  39070  toycom  40167  osumcllem7N  41156  pexmidlem4N  41167  diaintclN  42252  dibintclN  42361  mapd1o  42842  hdmapevec  43029  dvrelog2  43251  aks6d1c2lem4  43314  sticksstones1  43333  aks6d1c6lem5  43364  redvmptabs  43548  imacrhmcl  43718  prjspvs  43775  prjspeclsp  43777  0prjspnrel  43800  elrfi  43842  elrfirn  43843  elrfirn2  43844  mrefg3  43856  diophin  43920  diophun  43921  eq0rabdioph  43924  eqrabdioph  43925  pellex  43979  rmxycomplete  44061  jm2.23  44140  aomclem2  44194  fglmod  44212  lsmfgcl  44213  lmhmfgima  44223  lmhmfgsplit  44225  isnumbasabl  44245  dgrsub2  44274  itgocn  44303  areaquad  44355  cantnftermord  44459  omabs2  44471  nna1iscard  44683  elmapintrab  44714  corcltrcl  44876  radcnvrat  45435  uzmptshftfval  45467  binomcxplemdvsum  45476  binomcxplemnotnn0  45477  onfrALTlem2  45665  onfrALTlem2VD  46007  uzwo4  46206  mptssid  46389  uzublem  46576  eliccelioc  46669  elicores  46681  sqrlearg  46701  fsumiunss  46723  limcdm0  46766  sumnnodd  46778  fnlimfvre  46820  limsupubuzlem  46858  limsupmnflem  46866  limsupre3uzlem  46881  climuzlem  46889  liminflelimsuplem  46921  cncfshift  47020  cncfperiod  47025  icccncfext  47033  dvnprodlem1  47092  dvnprodlem2  47093  itgsin0pilem1  47096  itgsinexplem1  47100  itgsinexp  47101  ditgeqiooicc  47106  itgsubsticclem  47121  itgioocnicc  47123  itgsbtaddcnst  47128  stoweidlem34  47180  stoweidlem41  47187  stoweidlem51  47197  wallispilem2  47212  stirlinglem11  47230  dirkercncflem2  47250  fourierdlem5  47258  fourierdlem9  47262  fourierdlem17  47270  fourierdlem18  47271  fourierdlem20  47273  fourierdlem39  47292  fourierdlem48  47300  fourierdlem49  47301  fourierdlem62  47314  fourierdlem66  47318  fourierdlem68  47320  fourierdlem72  47324  fourierdlem73  47325  fourierdlem81  47333  fourierdlem83  47335  fourierdlem85  47337  fourierdlem87  47339  fourierdlem88  47340  fourierdlem92  47344  fourierdlem95  47347  fourierdlem103  47355  fourierdlem104  47356  fourierdlem112  47364  sqwvfoura  47374  sqwvfourb  47375  fouriersw  47377  etransclem24  47404  etransclem35  47415  etransclem37  47417  salexct  47480  salgencntex  47489  sge0resplit  47552  sge0split  47555  meaiuninclem  47626  caratheodorylem1  47672  volicorescl  47699  hoidmv1lelem3  47739  opnvonmbllem2  47779  ovolval2  47790  ovolval3  47793  ovolval4lem1  47795  ovolval4lem2  47796  smfaddlem1  47909  smflimlem2  47918  smfrec  47935  smfdiv  47943  smfsuplem1  47957  smfsuplem3  47959  et-ltneverrefl  48017  wrddrin  48033  wrddun  48035  chndrin  48038  chndun  48040  chnrrin  48043  chnrun  48045  tannpoly  48076  fcores  48273  elfz2nn  48528  rehalfge1  48545  spr0el  48700  nprmdvdsfacm1lem4  48844  nprmdvdsfacm1  48845  ppivalnnnprmge6  48847  bgoldbtbndlem2  49040  bgoldbtbndlem3  49041  bgoldbtbnd  49043  upgrimpthslem2  49142  stgredgiun  49192  isubgr3stgrlem7  49206  fldhmsubcALTV  49566  fvconst0ci  50141  fvconstdomi  50142  idfullsubc  50413  fulloppf  50415  fthoppf  50416  initopropdlemlem  50497