Theorem sseli 3934

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906

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 2148

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

This theorem is used by:  sselii  3935  sselid  3936  elun1  4135  elun2  4136  elopabr  5547  elopabran  5548  elopaelxp  5753  copsex2ga  5796  imadifssran  6204  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  7068  ofrfvalg  7692  ofval  7695  off  7702  nnon  7874  finds  7899  finds2  7901  eqopi  8028  op1steq  8036  dfoprab4  8058  bropopvvv  8091  bropfvvvv  8093  reldmtpos  8236  smores2  8347  frsuc  8430  unifpw  9319  cantnfp1lem1  9654  cantnfp1lem3  9656  r1fin  9752  r1tr  9755  r1ordg  9757  r1ord3g  9758  r1val1  9765  tz9.12lem3  9768  tcrank  9863  elscottab  9878  cplem1  9886  cplem1OLD  9887  hta  9898  htaOLD  9899  tskwe  9952  cardprclem  9981  alephfplem3  10106  dfac12r  10146  ackbij1lem16  10233  ackbij2  10241  fin23lem28  10339  fin23lem30  10341  fin23lem31  10342  fin1a2lem6  10404  hsmexlem4  10428  hsmexlem5  10429  hsmexlem6  10430  axdc2lem  10447  axdc3lem2  10450  axcclem  10456  brdom5  10528  brdom4  10529  r1tskina  10782  gruina  10818  grur1a  10819  pinn  10878  0nnq  10924  elpqn  10925  recn  11205  rexr  11270  ltord1  11755  leord1  11756  eqord1  11757  nnre  12255  nncn  12256  nnind  12266  nnnn0  12526  nn0re  12528  nn0cn  12529  nn0xnn0  12596  nn0z  12630  uzuzle35  12927  nnq  13002  qcn  13003  rpre  13041  eliccxr  13478  difreicc  13527  iccshftri  13530  iccshftli  13532  iccdili  13534  icccntri  13536  fzval2  13554  fzelp1  13621  4fvwrd4  13693  elfzo1  13758  ico01fl0  13870  expcllem  14126  expcl2lem  14127  m1expcl2  14139  bcm1k  14369  bcpasc  14375  hashbclem  14507  wrdv  14584  pfxfv0  14751  pfxfvlsw  14754  cshimadifsn  14890  swrds2m  15002  01sqrexlem5  15321  cau3lem  15430  caubnd  15434  climconst2  15623  o1of2  15688  o1rlimmul  15694  caurcvg  15752  caucvg  15754  binomlem  15906  incexclem  15913  divcnvshft  15932  zprod  16014  fprodge1  16072  risefaccllem  16090  fallfaccllem  16091  bpolydiflem  16130  bpoly4  16135  dvdsflip  16397  divalglem8  16480  sadadd  16547  smumul  16573  isprm3  16763  phimullem  16860  prmdiveq  16867  unbenlem  16990  vdwnnlem1  17077  vdwnnlem3  17079  ramtcl2  17093  prmgaplem4  17136  cshwshashlem1  17177  structcnvcnv  17235  fvsetsid  17250  imasdsval2  17592  mreunirn  17675  mrcfval  17686  mrisval  17708  coapm  18150  tsrss  18667  chnccat  18704  ex-chn1  18715  submnd0OLD  18858  smndex1id  19010  nmzsubg  19275  nmznsg  19278  cntzmhm  19455  symgtrinv  19586  pmtrdifellem4  19593  psgnpmtr  19624  efginvrel2  19841  efginvrel1  19842  efgsp1  19851  efgsres  19852  efgsfo  19853  frgpinv  19878  frgpupf  19887  frgpup1  19889  subcmn  19951  torsubg  19968  dprd2dlem1  20157  dpjidcl  20174  ablfaclem3  20203  nzrring  20663  lringnzr  20690  fldhmsubc  20938  acsfn1p  20952  lssacs  21138  cnsubdrglem  21618  rege0subm  21623  rge0srg  21638  zringunit  21666  znrrg  21765  psgnghm  21780  zrhpsgnevpm  21791  evpmodpmf1o  21796  pmtrodpm  21797  phlssphl  21859  frlmsslsp  21996  islinds4  22035  lmimlbs  22036  lbslcic  22041  psrbaglefi  22126  psrbagconf1o  22129  mplsubglem  22198  mplneg  22209  ressmpladd  22229  ressmplmul  22230  ressmplvsca  22231  mplmonmul  22237  psdmul  22379  ply1bascl  22413  mdetralt  22815  mdetunilem7  22825  chfacfpmmulgsum2  23072  tgval2  23163  ordtbas  23399  ordtrestixx  23429  hauslly  23700  kgentop  23750  ptbasin  23785  filunirn  24090  uzrest  24105  elflim  24179  flffval  24197  fclsval  24216  isfcls  24217  fcfval  24241  ustn0  24429  fmucndlem  24498  xmetunirn  24545  mopnval  24646  setsmstopn  24686  tmsval  24689  tngtopn  24858  qtopbaslem  24966  xrtgioo  25015  reperflem  25027  icccmplem1  25031  icopnfhmeo  25153  icccvx  25160  bndth  25168  pcoval1  25223  pcoval2  25226  pcoass  25234  pcorevlem  25236  pcorev2  25238  pi1xfrcnv  25267  csscld  25459  cfilfval  25474  caufval  25485  bcthlem1  25534  ivthlem1  25661  ivthlem3  25663  ovolicc2lem3  25729  ovolicc2lem4  25730  vitalilem1  25818  mbflimsup  25876  i1fd  25891  i1f0  25897  i1f1  25900  itg1addlem4  25909  itg1addlem5  25910  iblmbf  25977  ellimc2  26087  limcres  26096  limcun  26105  dvbsss  26112  perfdvf  26113  dvres2lem  26120  dvaddbr  26148  rolle  26200  cmvth  26201  dvlip  26203  dvlipcn  26204  dvle  26217  lhop1lem  26223  dvfsumle  26231  dvfsumge  26232  dvfsumabs  26233  dvfsumlem2  26237  ftc2  26254  itgparts  26257  itgsubstlem  26258  itgsubst  26259  deg1mul3  26324  coeval  26431  coeeu  26433  dgrval  26436  coef3  26440  coemulc  26463  dgrsub  26480  coecj  26486  coecjOLD  26488  dvply2  26498  dvnply  26500  quotval  26504  fta1  26520  plyexmo  26525  aacjcl  26541  taylfval  26573  dvtaylp  26584  abelth  26655  pilem3  26667  cos0pilt1  26748  sinord  26750  recosf1o  26751  resinf1o  26752  tanord1  26753  eff1olem  26764  dvloglem  26864  dvlog  26867  dvlog2lem  26868  advlogexp  26871  logtayl  26876  logtayl2  26878  dvcncxp1  26959  dvcnsqrt  26960  cxpcn3lem  26963  cxpcn3  26964  sqrtcn  26966  loglesqrt  26977  1cubr  27058  acosrecl  27119  efrlim  27185  jensen  27204  lgamgulmlem2  27245  lgamucov2  27254  basellem4  27299  musum  27406  mpodvdsmulf1o  27409  fsumdvdsmul  27410  dchrinvcl  27468  dchrghm  27471  dchrinv  27476  dchrsum2  27483  dchrsum  27484  rpvmasumlem  27702  dchrisum0lem2a  27732  pnt  27829  oldf  28081  madeno  28087  oldno  28088  newno  28089  oldmade  28112  leftold  28119  rightold  28120  leftno  28121  rightno  28122  addbdaylem  28261  addbday  28262  negsproplem2  28273  negsid  28285  negsunif  28299  mulsproplem12  28371  mulsproplem13  28372  mulsproplem14  28373  precsexlem11  28461  onno  28499  oncutlt  28508  n0no  28567  nnno  28568  nnn0s  28571  nnsgt0  28583  zno  28626  expscllem  28674  tglng  28866  axlowdimlem6  29352  axlowdimlem16  29362  axlowdimlem17  29363  axlowdim  29366  axeuclidlem  29367  axcontlem2  29370  axcontlem7  29375  axcontlem8  29376  nbusgrvtxm1uvtx  29813  wlk1walk  30046  pthdivtx  30139  pthdadjvtx  30140  crctcshwlkn0lem2  30227  crctcshwlkn0lem4  30229  clwwisshclwws  30433  fusgreg2wsp  30758  nvvcop  31017  nvex  31034  phnv  31237  sheli  31637  cheli  31655  hhssabloilem  31684  choc1  31750  shintcli  31752  chintcli  31754  shsleji  31793  pjini  32122  mayete3i  32151  dmadjop  32311  nlelshi  32483  cnlnadjeui  32500  cnlnssadj  32503  bdopadj  32505  pjimai  32599  stcl  32639  atelch  32767  fcnvgreu  33088  f1od2  33134  fcobijfs  33136  fcobijfs2  33137  uzssico  33199  iundisj2fi  33212  nnindf  33234  eliccioo  33320  gsummptres  33436  cyc3genpm  33536  elrspunidl  33800  0mplrim  33968  psrmonmul  34004  zarcls  34328  ordtrestNEW  34375  xrge0iifcnv  34387  xrge0iifcv  34388  xrge0iifiso  34389  xrge0iifhom  34391  qqhcn  34445  esumval  34500  gsumesum  34513  esumlub  34514  esumcst  34517  esumfsup  34524  issgon  34577  elrnsiga  34580  imambfm  34717  br2base  34724  sxbrsigalem0  34726  dya2iocucvr  34739  sxbrsigalem2  34741  sxbrsigalem5  34743  sxbrsiga  34745  omssubadd  34755  sitmcl  34806  oddpwdc  34809  eulerpartlemelr  34812  eulerpartlemgvv  34831  eulerpartlemgh  34833  eulerpartlemgs2  34835  eulerpartlemn  34836  sseqf  34847  ballotlem2  34944  ballotlemfp1  34947  ballotlemfc0  34948  ballotlemfcc  34949  ballotlemfmpn  34950  ballotlemsup  34960  ballotlemfrceq  34984  signswch  35013  rpsqrtcn  35045  prodfzo03  35055  itgexpif  35058  bnj1533  35305  bnj1137  35448  bnj1286  35472  bnj1408  35489  bnj1417  35494  r1omhf  35558  onvf1odlem4  35647  subfacp1lem5  35713  cvmsi  35794  gonar  35924  goalr  35926  mpst123  36069  mpstrcl  36070  msrrcl  36072  elmsta  36077  msubvrs  36089  elmpps  36102  elmthm  36105  bcprod  36267  dfon2lem4  36313  pprodss4v  36411  ivthALT  36903  neibastop2lem  36928  nnssi2  37023  nnssi3  37024  ttcel2  37069  bj-sngltagi  37675  bj-elid5  37870  bj-fvmptunsn1  37958  bj-smgrpssmgmel  37970  bj-mndsssmgrpel  37972  bj-cmnssmndel  37974  bj-grpssmndel  37976  bj-ablssgrpel  37978  bj-ablsscmnel  37980  bj-vecssmodel  37983  bj-flddrng  37990  bj-rveccvec  38006  bj-rvecabl  38008  taupilemrplb  38021  icorempo  38054  elxp8  38074  sin2h  38318  cos2h  38319  tan2h  38320  poimirlem14  38342  poimirlem26  38354  poimirlem27  38355  poimirlem31  38359  poimirlem32  38360  mblfinlem1  38365  cnambfre  38376  dvtan  38378  itg2addnc  38382  itg2gt0cn  38383  ftc1cnnc  38400  ftc2nc  38410  dvasin  38412  dvacos  38413  cover2  38424  sstotbnd2  38483  heibor1lem  38518  heiborlem10  38529  opidonOLD  38561  exidcl  38585  rngosn3  38633  flddivrng  38708  toycom  39805  osumcllem7N  40794  pexmidlem4N  40805  diaintclN  41890  dibintclN  41999  mapd1o  42480  hdmapevec  42667  dvrelog2  42889  aks6d1c2lem4  42952  sticksstones1  42971  aks6d1c6lem5  43002  redvmptabs  43179  imacrhmcl  43346  prjspvs  43400  prjspeclsp  43402  0prjspnrel  43417  elrfi  43483  elrfirn  43484  elrfirn2  43485  mrefg3  43497  diophin  43561  diophun  43562  eq0rabdioph  43565  eqrabdioph  43566  pellex  43620  rmxycomplete  43702  jm2.23  43781  aomclem2  43840  fglmod  43858  lsmfgcl  43859  lmhmfgima  43869  lmhmfgsplit  43871  isnumbasabl  43891  dgrsub2  43920  itgocn  43949  areaquad  44001  cantnftermord  44105  omabs2  44117  nna1iscard  44329  elmapintrab  44360  corcltrcl  44523  k0004val0  44938  radcnvrat  45082  uzmptshftfval  45114  binomcxplemdvsum  45123  binomcxplemnotnn0  45124  onfrALTlem2  45313  onfrALTlem2VD  45655  uzwo4  45831  mptssid  46014  uzublem  46202  eliccelioc  46295  elicores  46307  sqrlearg  46327  fsumiunss  46349  limcdm0  46392  sumnnodd  46404  fnlimfvre  46446  limsupubuzlem  46484  limsupmnflem  46492  limsupre3uzlem  46507  climuzlem  46515  liminflelimsuplem  46547  cncfshift  46646  cncfperiod  46651  icccncfext  46659  dvnprodlem1  46718  dvnprodlem2  46719  itgsin0pilem1  46722  itgsinexplem1  46726  itgsinexp  46727  ditgeqiooicc  46732  itgsubsticclem  46747  itgioocnicc  46749  itgsbtaddcnst  46754  stoweidlem34  46806  stoweidlem41  46813  stoweidlem51  46823  wallispilem2  46838  stirlinglem11  46856  dirkercncflem2  46876  fourierdlem5  46884  fourierdlem9  46888  fourierdlem17  46896  fourierdlem18  46897  fourierdlem20  46899  fourierdlem39  46918  fourierdlem48  46926  fourierdlem49  46927  fourierdlem62  46940  fourierdlem66  46944  fourierdlem68  46946  fourierdlem72  46950  fourierdlem73  46951  fourierdlem81  46959  fourierdlem83  46961  fourierdlem85  46963  fourierdlem87  46965  fourierdlem88  46966  fourierdlem92  46970  fourierdlem95  46973  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  sqwvfoura  47000  sqwvfourb  47001  fouriersw  47003  etransclem24  47030  etransclem35  47041  etransclem37  47043  salexct  47106  salgencntex  47115  sge0resplit  47178  sge0split  47181  meaiuninclem  47252  caratheodorylem1  47298  volicorescl  47325  hoidmv1lelem3  47365  opnvonmbllem2  47405  ovolval2  47416  ovolval3  47419  ovolval4lem1  47421  ovolval4lem2  47422  smfaddlem1  47535  smflimlem2  47544  smfrec  47561  smfdiv  47569  smfsuplem1  47583  smfsuplem3  47585  et-ltneverrefl  47643  natglobalincr  47651  tannpoly  47685  fcores  47862  elfz2nn  48117  rehalfge1  48134  spr0el  48289  nprmdvdsfacm1lem4  48433  nprmdvdsfacm1  48434  ppivalnnnprmge6  48436  bgoldbtbndlem2  48629  bgoldbtbndlem3  48630  bgoldbtbnd  48632  upgrimpthslem2  48731  stgredgiun  48781  isubgr3stgrlem7  48795  fldhmsubcALTV  49155  fvconst0ci  49726  fvconstdomi  49727  idfullsubc  49996  fulloppf  49998  fthoppf  49999  initopropdlemlem  50074