Theorem sseli 3932

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837  df-ss 3921

This theorem is referenced by:  sselii  3933  sselid  3934  elun1  4134  elun2  4135  elopabr  5531  elopabran  5532  elopaelxp  5737  copsex2ga  5780  2elresin  6642  nfvres  6905  fvco4i  6969  mptrcl  6985  fvmptss  6988  fvmptex  6990  fvmptnf  6998  elfvmptrab1w  7003  elfvmptrab1  7004  fvopab4ndm  7006  fvimacnvi  7033  elpreima  7039  iinpreima  7050  ofrfvalg  7668  ofval  7671  off  7678  nnon  7852  finds  7877  finds2  7879  eqopi  8006  op1steq  8014  dfoprab4  8036  bropopvvv  8069  bropfvvvv  8071  reldmtpos  8214  smores2  8325  frsuc  8408  unifpw  9298  cantnfp1lem1  9633  cantnfp1lem3  9635  r1fin  9731  r1tr  9734  r1ordg  9736  r1ord3g  9737  r1val1  9744  tz9.12lem3  9747  tcrank  9842  cplem1  9847  hta  9855  tskwe  9908  cardprclem  9937  alephfplem3  10062  dfac12r  10103  ackbij1lem16  10190  ackbij2  10198  fin23lem28  10297  fin23lem30  10299  fin23lem31  10300  fin1a2lem6  10362  hsmexlem4  10386  hsmexlem5  10387  hsmexlem6  10388  axdc2lem  10405  axdc3lem2  10408  axcclem  10414  brdom5  10486  brdom4  10487  r1tskina  10740  gruina  10776  grur1a  10777  pinn  10836  0nnq  10882  elpqn  10883  recn  11163  rexr  11228  ltord1  11713  leord1  11714  eqord1  11715  nnre  12217  nncn  12218  nnind  12228  nnnn0  12488  nn0re  12490  nn0cn  12491  nn0xnn0  12558  nn0z  12592  uzuzle35  12888  nnq  12963  qcn  12964  rpre  13002  eliccxr  13439  difreicc  13488  iccshftri  13491  iccshftli  13493  iccdili  13495  icccntri  13497  fzval2  13515  fzelp1  13581  4fvwrd4  13653  elfzo1  13718  ico01fl0  13829  expcllem  14085  expcl2lem  14086  m1expcl2  14098  bcm1k  14328  bcpasc  14334  hashbclem  14465  wrdv  14542  pfxfv0  14705  pfxfvlsw  14708  cshimadifsn  14842  swrds2m  14954  01sqrexlem5  15273  cau3lem  15382  caubnd  15386  climconst2  15575  o1of2  15640  o1rlimmul  15646  caurcvg  15704  caucvg  15706  binomlem  15859  incexclem  15866  divcnvshft  15885  zprod  15967  fprodge1  16025  risefaccllem  16043  fallfaccllem  16044  bpolydiflem  16084  bpoly4  16089  dvdsflip  16351  divalglem8  16434  sadadd  16501  smumul  16527  isprm3  16717  phimullem  16814  prmdiveq  16821  unbenlem  16944  vdwnnlem1  17031  vdwnnlem3  17033  ramtcl2  17047  prmgaplem4  17090  cshwshashlem1  17131  structcnvcnv  17189  fvsetsid  17204  imasdsval2  17546  mreunirn  17629  mrcfval  17640  mrisval  17662  coapm  18104  tsrss  18621  chnccat  18658  ex-chn1  18669  submnd0  18797  smndex1id  18948  nmzsubg  19206  nmznsg  19209  cntzmhm  19381  symgtrinv  19512  pmtrdifellem4  19519  psgnpmtr  19550  efginvrel2  19767  efginvrel1  19768  efgsp1  19777  efgsres  19778  efgsfo  19779  frgpinv  19804  frgpupf  19813  frgpup1  19815  subcmn  19877  torsubg  19894  dprd2dlem1  20083  dpjidcl  20100  ablfaclem3  20129  nzrring  20562  lringnzr  20587  fldhmsubc  20831  acsfn1p  20845  lssacs  21031  cnsubdrglem  21467  rege0subm  21472  rge0srg  21487  zringunit  21515  znrrg  21614  psgnghm  21629  zrhpsgnevpm  21640  evpmodpmf1o  21645  pmtrodpm  21646  phlssphl  21708  frlmsslsp  21845  islinds4  21884  lmimlbs  21885  lbslcic  21890  psrbaglefi  21975  psrbagconf1o  21978  mplsubglem  22047  mplneg  22058  ressmpladd  22078  ressmplmul  22079  ressmplvsca  22080  mplmonmul  22086  psdmul  22228  ply1bascl  22262  mdetralt  22665  mdetunilem7  22675  chfacfpmmulgsum2  22922  tgval2  23013  ordtbas  23249  ordtrestixx  23279  hauslly  23549  kgentop  23599  ptbasin  23634  filunirn  23939  uzrest  23954  elflim  24028  flffval  24046  fclsval  24065  isfcls  24066  fcfval  24090  ustn0  24278  fmucndlem  24347  xmetunirn  24394  mopnval  24495  setsmstopn  24535  tmsval  24538  tngtopn  24707  qtopbaslem  24815  xrtgioo  24864  reperflem  24876  icccmplem1  24880  icopnfhmeo  25002  icccvx  25009  bndth  25017  pcoval1  25072  pcoval2  25075  pcoass  25083  pcorevlem  25085  pcorev2  25087  pi1xfrcnv  25116  csscld  25308  cfilfval  25323  caufval  25334  bcthlem1  25383  ivthlem1  25510  ivthlem3  25512  ovolicc2lem3  25578  ovolicc2lem4  25579  vitalilem1  25667  mbflimsup  25725  i1fd  25740  i1f0  25746  i1f1  25749  itg1addlem4  25758  itg1addlem5  25759  iblmbf  25826  ellimc2  25936  limcres  25945  limcun  25954  dvbsss  25961  perfdvf  25962  dvres2lem  25969  dvaddbr  25997  rolle  26049  cmvth  26050  dvlip  26052  dvlipcn  26053  dvle  26066  lhop1lem  26072  dvfsumle  26080  dvfsumge  26081  dvfsumabs  26082  dvfsumlem2  26086  ftc2  26103  itgparts  26106  itgsubstlem  26107  itgsubst  26108  deg1mul3  26173  coeval  26280  coeeu  26282  dgrval  26285  coef3  26289  coemulc  26312  dgrsub  26329  coecj  26335  coecjOLD  26337  dvply2  26347  dvnply  26349  quotval  26353  fta1  26369  plyexmo  26374  aacjcl  26388  taylfval  26419  dvtaylp  26430  abelth  26501  pilem3  26513  cos0pilt1  26594  sinord  26596  recosf1o  26597  resinf1o  26598  tanord1  26599  eff1olem  26610  dvloglem  26710  dvlog  26713  dvlog2lem  26714  advlogexp  26717  logtayl  26722  logtayl2  26724  dvcncxp1  26805  dvcnsqrt  26806  cxpcn3lem  26809  cxpcn3  26810  sqrtcn  26812  loglesqrt  26823  1cubr  26904  acosrecl  26965  efrlim  27031  jensen  27050  lgamgulmlem2  27091  lgamucov2  27100  basellem4  27145  musum  27252  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dchrinvcl  27314  dchrghm  27317  dchrinv  27322  dchrsum2  27329  dchrsum  27330  rpvmasumlem  27548  dchrisum0lem2a  27578  pnt  27675  oldf  27927  madeno  27933  oldno  27934  newno  27935  oldmade  27958  leftold  27965  rightold  27966  leftno  27967  rightno  27968  addbdaylem  28107  addbday  28108  negsproplem2  28119  negsid  28131  negsunif  28145  mulsproplem12  28217  mulsproplem13  28218  mulsproplem14  28219  precsexlem11  28307  onno  28345  oncutlt  28354  n0no  28413  nnno  28414  nnn0s  28417  nnsgt0  28429  zno  28472  expscllem  28520  tglng  28712  axlowdimlem6  29145  axlowdimlem16  29155  axlowdimlem17  29156  axlowdim  29159  axeuclidlem  29160  axcontlem2  29163  axcontlem7  29168  axcontlem8  29169  nbusgrvtxm1uvtx  29603  wlk1walk  29836  pthdivtx  29924  pthdadjvtx  29925  crctcshwlkn0lem2  30008  crctcshwlkn0lem4  30010  clwwisshclwws  30214  fusgreg2wsp  30535  nvvcop  30794  nvex  30811  phnv  31014  sheli  31414  cheli  31432  hhssabloilem  31461  choc1  31527  shintcli  31529  chintcli  31531  shsleji  31570  pjini  31899  mayete3i  31928  dmadjop  32088  nlelshi  32260  cnlnadjeui  32277  cnlnssadj  32280  bdopadj  32282  pjimai  32376  stcl  32416  atelch  32544  fcnvgreu  32871  f1od2  32918  fcobijfs  32920  fcobijfs2  32921  uzssico  32983  iundisj2fi  32996  nnindf  33019  eliccioo  33105  gsummptres  33229  cyc3genpm  33329  elrspunidl  33611  0mplrim  33808  psrmonmul  33844  zarcls  34168  ordtrestNEW  34215  xrge0iifcnv  34227  xrge0iifcv  34228  xrge0iifiso  34229  xrge0iifhom  34231  qqhcn  34285  esumval  34340  gsumesum  34353  esumlub  34354  esumcst  34357  esumfsup  34364  issgon  34417  elrnsiga  34420  imambfm  34556  br2base  34563  sxbrsigalem0  34565  dya2iocucvr  34578  sxbrsigalem2  34580  sxbrsigalem5  34582  sxbrsiga  34584  omssubadd  34594  sitmcl  34645  oddpwdc  34648  eulerpartlemelr  34651  eulerpartlemgvv  34670  eulerpartlemgh  34672  eulerpartlemgs2  34674  eulerpartlemn  34675  sseqf  34686  ballotlem2  34783  ballotlemfp1  34786  ballotlemfc0  34787  ballotlemfcc  34788  ballotlemfmpn  34789  ballotlemsup  34799  ballotlemfrceq  34823  signswch  34852  rpsqrtcn  34884  prodfzo03  34894  itgexpif  34897  bnj1533  35144  bnj1137  35287  bnj1286  35311  bnj1408  35328  bnj1417  35333  r1omhf  35399  onvf1odlem4  35446  subfacp1lem5  35531  cvmsi  35612  gonar  35742  goalr  35744  mpst123  35887  mpstrcl  35888  msrrcl  35890  elmsta  35895  msubvrs  35907  elmpps  35920  elmthm  35923  bcprod  36085  dfon2lem4  36131  pprodss4v  36229  ivthALT  36692  neibastop2lem  36717  nnssi2  36812  nnssi3  36813  ttcel2  36858  bj-sngltagi  37464  bj-elid5  37658  bj-fvmptunsn1  37746  bj-smgrpssmgmel  37758  bj-mndsssmgrpel  37760  bj-cmnssmndel  37762  bj-grpssmndel  37764  bj-ablssgrpel  37766  bj-ablsscmnel  37768  bj-vecssmodel  37771  bj-flddrng  37778  bj-rveccvec  37794  bj-rvecabl  37796  taupilemrplb  37809  icorempo  37842  elxp8  37862  sin2h  38106  cos2h  38107  tan2h  38108  poimirlem14  38130  poimirlem26  38142  poimirlem27  38143  poimirlem31  38147  poimirlem32  38148  mblfinlem1  38153  cnambfre  38164  dvtan  38166  itg2addnc  38170  itg2gt0cn  38171  ftc1cnnc  38188  ftc2nc  38198  dvasin  38200  dvacos  38201  cover2  38211  sstotbnd2  38270  heibor1lem  38305  heiborlem10  38316  opidonOLD  38348  exidcl  38372  rngosn3  38420  flddivrng  38495  toycom  39594  osumcllem7N  40583  pexmidlem4N  40594  diaintclN  41679  dibintclN  41788  mapd1o  42269  hdmapevec  42456  dvrelog2  42678  aks6d1c2lem4  42741  sticksstones1  42760  aks6d1c6lem5  42791  redvmptabs  42966  imacrhmcl  43133  prjspvs  43189  prjspeclsp  43191  0prjspnrel  43206  elrfi  43272  elrfirn  43273  elrfirn2  43274  mrefg3  43286  diophin  43350  diophun  43351  eq0rabdioph  43354  eqrabdioph  43355  pellex  43409  rmxycomplete  43491  jm2.23  43570  aomclem2  43629  fglmod  43647  lsmfgcl  43648  lmhmfgima  43658  lmhmfgsplit  43660  isnumbasabl  43680  dgrsub2  43709  itgocn  43738  areaquad  43790  cantnftermord  43894  omabs2  43906  nna1iscard  44118  elmapintrab  44149  corcltrcl  44312  k0004val0  44727  elscottab  44817  radcnvrat  44887  uzmptshftfval  44919  binomcxplemdvsum  44928  binomcxplemnotnn0  44929  onfrALTlem2  45119  onfrALTlem2VD  45461  uzwo4  45630  mptssid  45813  uzublem  46001  eliccelioc  46094  elicores  46106  sqrlearg  46126  fsumiunss  46148  limcdm0  46191  sumnnodd  46203  fnlimfvre  46245  limsupubuzlem  46283  limsupmnflem  46291  limsupre3uzlem  46306  climuzlem  46314  liminflelimsuplem  46346  cncfshift  46445  cncfperiod  46450  icccncfext  46458  dvnprodlem1  46517  dvnprodlem2  46518  itgsin0pilem1  46521  itgsinexplem1  46525  itgsinexp  46526  ditgeqiooicc  46531  itgsubsticclem  46546  itgioocnicc  46548  itgsbtaddcnst  46553  stoweidlem34  46605  stoweidlem41  46612  stoweidlem51  46622  wallispilem2  46637  stirlinglem11  46655  dirkercncflem2  46675  fourierdlem5  46683  fourierdlem9  46687  fourierdlem17  46695  fourierdlem18  46696  fourierdlem20  46698  fourierdlem39  46717  fourierdlem48  46725  fourierdlem49  46726  fourierdlem62  46739  fourierdlem66  46743  fourierdlem68  46745  fourierdlem72  46749  fourierdlem73  46750  fourierdlem81  46758  fourierdlem83  46760  fourierdlem85  46762  fourierdlem87  46764  fourierdlem88  46765  fourierdlem92  46769  fourierdlem95  46772  fourierdlem103  46780  fourierdlem104  46781  fourierdlem112  46789  sqwvfoura  46799  sqwvfourb  46800  fouriersw  46802  etransclem24  46829  etransclem35  46840  etransclem37  46842  salexct  46905  salgencntex  46914  sge0resplit  46977  sge0split  46980  meaiuninclem  47051  caratheodorylem1  47097  volicorescl  47124  hoidmv1lelem3  47164  opnvonmbllem2  47204  ovolval2  47215  ovolval3  47218  ovolval4lem1  47220  ovolval4lem2  47221  smfaddlem1  47334  smflimlem2  47343  smfrec  47360  smfdiv  47368  smfsuplem1  47382  smfsuplem3  47384  et-ltneverrefl  47442  natglobalincr  47450  tannpoly  47481  fcores  47658  elfz2nn  47913  rehalfge1  47930  spr0el  48085  nprmdvdsfacm1lem4  48229  nprmdvdsfacm1  48230  ppivalnnnprmge6  48232  bgoldbtbndlem2  48425  bgoldbtbndlem3  48426  bgoldbtbnd  48428  upgrimpthslem2  48527  stgredgiun  48577  isubgr3stgrlem7  48591  fldhmsubcALTV  48952  fvconst0ci  49509  fvconstdomi  49510  idfullsubc  49779  fulloppf  49781  fthoppf  49782  initopropdlemlem  49857