Theorem sseli 3909

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  sselii  3910  sselid  3911  elun1  4183  elun2  4184  elopabr  5542  elopabran  5543  elopaelxp  5749  copsex2ga  5794  imadifssranOLD  6221  2elresin  6690  nfvres  6954  fvco4i  7018  mptrcl  7034  fvmptss  7037  fvmptex  7039  fvmptnf  7047  elfvmptrab1w  7052  elfvmptrab1  7053  fvopab4ndm  7055  fvimacnvi  7082  elpreima  7088  elpreimaOLD  7089  iinpreima  7101  ofrfvalg  7733  ofval  7736  off  7743  nnon  7917  finds  7942  finds2  7944  eqopi  8071  op1steq  8079  dfoprab4  8101  bropopvvv  8136  bropfvvvv  8138  f1od2  8145  reldmtpos  8289  smores2  8400  frsuc  8483  unifpw  9382  cantnfp1lem1  9716  cantnfp1lem3  9718  r1fin  9817  r1tr  9820  r1ordg  9822  r1ord3g  9823  r1val1  9830  tz9.12lem3  9833  tcrank  9938  elscottab  9979  cplem1  9987  cplem1OLD  9988  hta  9999  htaOLD  10000  tskwe  10068  cardprclem  10097  alephfplem3  10224  dfac12r  10264  ackbij1lem16  10351  ackbij2  10359  fin23lem28  10457  fin23lem30  10459  fin23lem31  10460  fin1a2lem6  10522  hsmexlem4  10546  hsmexlem5  10547  hsmexlem6  10548  axdc2lem  10565  axdc3lem2  10568  axcclem  10574  brdom5  10647  brdom4  10648  r1tskina  10906  gruina  10942  grur1a  10943  pinn  11002  0nnq  11048  elpqn  11049  recn  11329  rexr  11394  ltord1  11882  leord1  11883  eqord1  11884  nnre  12382  nncn  12383  nnind  12393  nnnn0  12653  nn0re  12655  nn0cn  12656  nn0xnn0  12723  nn0z  12757  uzuzle35  13054  nnq  13129  qcn  13130  rpre  13169  eliccxr  13606  difreicc  13655  iccshftri  13658  iccshftli  13660  iccdili  13662  icccntri  13664  fzval2  13682  fzelp1  13750  4fvwrd4  13822  elfzo1  13887  ico01fl0  13999  expcllem  14255  expcl2lem  14256  m1expcl2  14268  bcm1k  14500  bcpasc  14506  hashbclem  14638  wrdv  14715  pfxfv0  14883  pfxfvlsw  14886  cshimadifsn  15022  swrds2m  15135  01sqrexlem5  15456  cau3lem  15566  caubnd  15570  climconst2  15759  o1of2  15824  o1rlimmul  15830  caurcvg  15888  caucvg  15890  binomlem  16042  incexclem  16049  divcnvshft  16068  zprod  16148  fprodge1  16206  risefaccllem  16224  fallfaccllem  16225  bpolydiflem  16264  bpoly4  16269  dvdsflip  16531  divalglem8  16614  sadadd  16681  smumul  16707  isprm3  16902  phimullem  17000  prmdiveq  17007  unbenlem  17130  vdwnnlem1  17217  vdwnnlem3  17219  ramtcl2  17233  prmgaplem4  17276  cshwshashlem1  17317  structcnvcnv  17375  fvsetsid  17390  imasdsval2  17738  mreunirn  17821  mrcfval  17832  mrisval  17854  coapm  18296  tsrss  18813  chnccat  18850  ex-chn1  18861  submnd0OLD  19007  smndex1id  19160  nmzsubg  19425  nmznsg  19428  cntzmhm  19606  symgtrinv  19737  pmtrdifellem4  19744  psgnpmtr  19775  efginvrel2  19992  efginvrel1  19993  efgsp1  20002  efgsres  20003  efgsfo  20004  frgpinv  20029  frgpupf  20038  frgpup1  20040  subcmn  20102  torsubg  20119  dprd2dlem1  20308  dpjidcl  20325  ablfaclem3  20354  nzrring  20817  lringnzr  20844  fldhmsubc  21093  acsfn1p  21107  lssacs  21293  cnsubdrglem  21776  rege0subm  21783  rge0srg  21798  zringunit  21827  znrrg  21926  psgnghm  21941  zrhpsgnevpm  21952  evpmodpmf1o  21957  pmtrodpm  21958  phlssphl  22020  frlmsslsp  22157  islinds4  22196  lmimlbs  22197  lbslcic  22202  psrbaglefi  22289  psrbagconf1o  22292  mplsubglem  22361  mplneg  22372  ressmpladd  22392  ressmplmul  22393  ressmplvsca  22394  mplmonmul  22400  psdmul  22542  ply1bascl  22576  mdetralt  22978  mdetunilem7  22988  chfacfpmmulgsum2  23238  tgval2  23329  ordtbas  23565  ordtrestixx  23595  hauslly  23866  kgentop  23916  ptbasin  23951  filunirn  24256  uzrest  24271  elflim  24345  flffval  24363  fclsval  24382  isfcls  24383  fcfval  24407  ustn0  24595  fmucndlem  24664  xmetunirn  24711  mopnval  24812  setsmstopn  24852  tmsval  24855  tngtopn  25024  qtopbaslem  25132  xrtgioo  25181  reperflem  25193  icccmplem1  25197  icopnfhmeo  25319  icccvx  25326  bndth  25334  pcoval1  25389  pcoval2  25392  pcoass  25400  pcorevlem  25402  pcorev2  25404  pi1xfrcnv  25433  csscld  25625  cfilfval  25640  caufval  25651  bcthlem1  25700  ivthlem1  25827  ivthlem3  25829  ovolicc2lem3  25895  ovolicc2lem4  25896  vitalilem1  25984  mbflimsup  26042  i1fd  26057  i1f0  26063  i1f1  26066  itg1addlem4  26075  itg1addlem5  26076  iblmbf  26143  ellimc2  26252  limcres  26261  limcun  26270  dvbsss  26277  perfdvf  26278  dvres2lem  26285  dvaddbr  26313  rolle  26365  cmvth  26366  dvlip  26368  dvlipcn  26369  dvle  26382  lhop1lem  26388  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  dvfsumlem2  26402  ftc2  26419  itgparts  26422  itgsubstlem  26423  itgsubst  26424  deg1mul3  26489  coeval  26597  coeeu  26599  dgrval  26602  coef3  26606  coemulc  26629  dgrsub  26646  coecj  26652  dvply2  26662  dvnply  26664  quotval  26668  fta1  26684  plyexmo  26691  aacjcl  26711  taylfval  26743  dvtaylp  26754  abelth  26825  pilem3  26837  cos0pilt1  26917  sinord  26919  recosf1o  26920  resinf1o  26921  tanord1  26922  eff1olem  26933  dvloglem  27033  dvlog  27036  dvlog2lem  27037  advlogexp  27040  logtayl  27045  logtayl2  27047  dvcncxp1  27128  dvcnsqrt  27129  cxpcn3lem  27132  cxpcn3  27133  sqrtcn  27135  loglesqrt  27146  1cubr  27227  acosrecl  27288  efrlim  27354  jensen  27373  lgamgulmlem2  27414  lgamucov2  27423  basellem4  27468  musum  27575  mpodvdsmulf1o  27578  fsumdvdsmul  27579  dchrinvcl  27637  dchrghm  27640  dchrinv  27645  dchrsum2  27652  dchrsum  27653  rpvmasumlem  27871  dchrisum0lem2a  27901  pnt  27998  oldf  28280  madeno  28286  oldno  28287  newno  28288  oldmade  28311  leftold  28318  rightold  28319  leftno  28320  rightno  28321  addbdaylem  28460  addbday  28461  negsproplem2  28472  negsid  28484  negsunif  28498  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  precsexlem11  28660  onno  28698  oncutlt  28707  n0no  28766  nnno  28767  nnn0s  28770  nnsgt0  28782  zno  28825  expscllem  28873  tglng  29066  axlowdimlem6  29582  axlowdimlem16  29592  axlowdimlem17  29593  axlowdim  29596  axeuclidlem  29597  axcontlem2  29600  axcontlem7  29605  axcontlem8  29606  nbusgrvtxm1uvtx  30043  wlk1walk  30276  pthdivtx  30369  pthdadjvtx  30370  crctcshwlkn0lem2  30457  crctcshwlkn0lem4  30459  clwwisshclwws  30663  fusgreg2wsp  30994  nvvcop  31253  nvex  31270  phnv  31473  sheli  31873  cheli  31891  hhssabloilem  31920  choc1  31986  shintcli  31988  chintcli  31990  shsleji  32029  pjini  32358  mayete3i  32387  dmadjop  32547  nlelshi  32719  cnlnadjeui  32736  cnlnssadj  32739  bdopadj  32741  pjimai  32835  stcl  32875  atelch  33003  fcnvgreu  33364  fcobijfs  33409  fcobijfs2  33410  uzssico  33472  iundisj2fi  33485  nnindf  33507  eliccioo  33593  gsummptres  33712  cyc3genpm  33812  elrspunidl  34082  0mplrim  34257  psrmonmul  34293  zarcls  34617  ordtrestNEW  34664  xrge0iifcnv  34676  xrge0iifcv  34677  xrge0iifiso  34678  xrge0iifhom  34680  qqhcn  34734  esumval  34789  gsumesum  34802  esumlub  34803  esumcst  34806  esumfsup  34813  issgon  34866  elrnsiga  34869  imambfm  35005  br2base  35012  sxbrsigalem0  35014  dya2iocucvr  35027  sxbrsigalem2  35029  sxbrsigalem5  35031  sxbrsiga  35033  omssubadd  35043  sitmcl  35094  oddpwdc  35097  eulerpartlemelr  35100  eulerpartlemgvv  35119  eulerpartlemgh  35121  eulerpartlemgs2  35123  eulerpartlemn  35124  sseqf  35135  ballotlem2  35232  ballotlemfp1  35235  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemfmpn  35238  ballotlemsup  35248  ballotlemfrceq  35272  signswch  35301  rpsqrtcn  35333  prodfzo03  35343  itgexpif  35346  bnj1533  35593  bnj1137  35736  bnj1286  35760  bnj1408  35777  bnj1417  35782  acwer1prc  35893  onvf1odlem4  36075  subfacp1lem5  36157  cvmsi  36238  gonar  36368  goalr  36370  mpst123  36513  mpstrcl  36514  msrrcl  36516  elmsta  36521  msubvrs  36533  elmpps  36546  elmthm  36549  bcprod  36718  dfon2lem1  36760  dfon2lem4  36763  pprodss4v  36861  ivthALT  37338  neibastop2lem  37363  nnssi2  37458  nnssi3  37459  ttcel2  37504  bj-sngltagi  38110  bj-elid5  38358  bj-fvmptunsn1  38446  bj-smgrpssmgmel  38458  bj-mndsssmgrpel  38460  bj-cmnssmndel  38462  bj-grpssmndel  38464  bj-ablssgrpel  38466  bj-ablsscmnel  38468  bj-vecssmodel  38471  bj-flddrng  38478  bj-rveccvec  38494  bj-rvecabl  38496  taupilemrplb  38509  icorempo  38542  elxp8  38562  sin2h  38801  cos2h  38802  tan2h  38803  poimirlem14  38820  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  mblfinlem1  38843  cnambfre  38854  dvtan  38856  itg2addnc  38860  itg2gt0cn  38861  ftc1cnnc  38878  ftc2nc  38888  dvasin  38890  dvacos  38891  cover2  38917  sstotbnd2  38974  heibor1lem  39009  heiborlem10  39020  opidonOLD  39052  exidcl  39076  rngosn3  39124  flddivrng  39199  toycom  40296  osumcllem7N  41285  pexmidlem4N  41296  diaintclN  42381  dibintclN  42490  mapd1o  42971  hdmapevec  43158  dvrelog2  43380  aks6d1c2lem4  43443  sticksstones1  43462  aks6d1c6lem5  43493  redvmptabs  43677  imacrhmcl  43847  prjspvs  43904  prjspeclsp  43906  0prjspnrel  43929  elrfi  43971  elrfirn  43972  elrfirn2  43973  mrefg3  43985  diophin  44049  diophun  44050  eq0rabdioph  44053  eqrabdioph  44054  pellex  44108  rmxycomplete  44190  jm2.23  44269  aomclem2  44323  fglmod  44341  lsmfgcl  44342  lmhmfgima  44352  lmhmfgsplit  44354  isnumbasabl  44373  dgrsub2  44402  itgocn  44431  areaquad  44479  cantnftermord  44583  omabs2  44595  nna1iscard  44807  elmapintrab  44838  corcltrcl  45000  radcnvrat  45559  uzmptshftfval  45591  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  onfrALTlem2  45789  onfrALTlem2VD  46131  uzwo4  46344  mptssid  46526  uzublem  46713  eliccelioc  46806  elicores  46818  sqrlearg  46838  fsumiunss  46860  limcdm0  46903  sumnnodd  46915  fnlimfvre  46957  limsupubuzlem  46995  limsupmnflem  47003  limsupre3uzlem  47018  climuzlem  47026  liminflelimsuplem  47058  cncfshift  47157  cncfperiod  47162  icccncfext  47170  dvnprodlem1  47229  dvnprodlem2  47230  itgsin0pilem1  47233  itgsinexplem1  47237  itgsinexp  47238  ditgeqiooicc  47243  itgsubsticclem  47258  itgioocnicc  47260  itgsbtaddcnst  47265  stoweidlem34  47317  stoweidlem41  47324  stoweidlem51  47334  wallispilem2  47349  stirlinglem11  47367  dirkercncflem2  47387  fourierdlem5  47395  fourierdlem9  47399  fourierdlem17  47407  fourierdlem18  47408  fourierdlem20  47410  fourierdlem39  47429  fourierdlem48  47437  fourierdlem49  47438  fourierdlem62  47451  fourierdlem66  47455  fourierdlem68  47457  fourierdlem72  47461  fourierdlem73  47462  fourierdlem81  47470  fourierdlem83  47472  fourierdlem85  47474  fourierdlem87  47476  fourierdlem88  47477  fourierdlem92  47481  fourierdlem95  47484  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  sqwvfoura  47511  sqwvfourb  47512  fouriersw  47514  etransclem24  47541  etransclem35  47552  etransclem37  47554  salexct  47617  salgencntex  47626  sge0resplit  47689  sge0split  47692  meaiuninclem  47763  caratheodorylem1  47809  volicorescl  47836  hoidmv1lelem3  47876  opnvonmbllem2  47916  ovolval2  47927  ovolval3  47930  ovolval4lem1  47932  ovolval4lem2  47933  smfaddlem1  48046  smflimlem2  48055  smfrec  48072  smfdiv  48080  smfsuplem1  48094  smfsuplem3  48096  et-ltneverrefl  48154  wrddrin  48170  wrddun  48172  chndrin  48175  chndun  48177  chnrrin  48180  chnrun  48182  tannpoly  48213  fcores  48410  elfz2nn  48665  rehalfge1  48682  spr0el  48837  nprmdvdsfacm1lem4  48981  nprmdvdsfacm1  48982  ppivalnnnprmge6  48984  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbnd  49180  upgrimpthslem2  49279  stgredgiun  49329  isubgr3stgrlem7  49343  fldhmsubcALTV  49703  subrgccdom  49709  fvconst0ci  50336  fvconstdomi  50337  idfullsubc  50608  fulloppf  50610  fthoppf  50611  initopropdlemlem  50692