Theorem sseli 3883

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

Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  sselii  3884  sseldi  3885  elun1  4076  elun2  4077  elopabran  5427  copsex2ga  5662  2elresin  6476  nfvres  6731  fvco4i  6790  mptrcl  6805  fvmptss  6808  fvmptex  6810  fvmptnf  6818  elfvmptrab1w  6822  elfvmptrab1  6823  fvopab4ndm  6825  fvimacnvi  6850  elpreima  6856  iinpreima  6867  ofrfvalg  7454  ofval  7457  off  7464  nnon  7628  finds  7654  finds2  7656  eqopi  7775  op1steq  7783  dfoprab4  7803  bropopvvv  7836  bropfvvvv  7838  reldmtpos  7954  wfrlem10  8042  smores2  8069  frsuc  8150  nnfiOLD  8848  unifpw  8957  cantnfp1lem1  9271  cantnfp1lem3  9273  r1fin  9354  r1tr  9357  r1ordg  9359  r1ord3g  9360  r1val1  9367  tz9.12lem3  9370  tcrank  9465  cplem1  9470  hta  9478  tskwe  9531  cardprclem  9560  alephfplem3  9685  dfac12r  9725  ackbij1lem16  9814  ackbij2  9822  fin23lem28  9919  fin23lem30  9921  fin23lem31  9922  fin1a2lem6  9984  hsmexlem4  10008  hsmexlem5  10009  hsmexlem6  10010  axdc2lem  10027  axdc3lem2  10030  axcclem  10036  brdom5  10108  brdom4  10109  r1tskina  10361  gruina  10397  grur1a  10398  pinn  10457  0nnq  10503  elpqn  10504  recn  10784  rexr  10844  ltord1  11323  leord1  11324  eqord1  11325  nnre  11802  nncn  11803  nnind  11813  nnnn0  12062  nn0re  12064  nn0cn  12065  nn0xnn0  12131  nnz  12164  nn0z  12165  nnq  12523  qcn  12524  rpre  12559  eliccxr  12988  difreicc  13037  iccshftri  13040  iccshftli  13042  iccdili  13044  icccntri  13046  fzval2  13063  fzelp1  13129  4fvwrd4  13197  elfzo1  13257  ico01fl0  13359  expcllem  13611  expcl2lem  13612  m1expcl2  13622  bcm1k  13846  bcpasc  13852  hashbclem  13981  wrdv  14049  pfxfv0  14222  pfxfvlsw  14225  cshimadifsn  14359  swrds2m  14471  sqrlem5  14775  cau3lem  14883  caubnd  14887  climconst2  15074  o1of2  15139  o1rlimmul  15145  caurcvg  15205  caucvg  15207  binomlem  15356  incexclem  15363  divcnvshft  15382  zprod  15462  fprodge1  15520  risefaccllem  15538  fallfaccllem  15539  bpolydiflem  15579  bpoly4  15584  dvdsflip  15841  divalglem8  15924  sadadd  15989  smumul  16015  isprm3  16203  phimullem  16295  prmdiveq  16302  unbenlem  16424  vdwnnlem1  16511  vdwnnlem3  16513  ramtcl2  16527  prmgaplem4  16570  cshwshashlem1  16612  structcnvcnv  16680  fvsetsid  16697  imasdsval2  16975  mreunirn  17058  mrcfval  17065  mrisval  17087  coapm  17531  tsrss  18049  submnd0  18156  smndex1id  18292  nmzsubg  18535  nmznsg  18538  cntzmhm  18687  symgtrinv  18818  pmtrdifellem4  18825  psgnpmtr  18856  efginvrel2  19071  efginvrel1  19072  efgsp1  19081  efgsres  19082  efgsfo  19083  frgpinv  19108  frgpupf  19117  frgpup1  19119  subcmn  19176  torsubg  19193  dprd2dlem1  19382  dpjidcl  19399  ablfaclem3  19428  acsfn1p  19797  lssacs  19958  cnsubdrglem  20368  rege0subm  20373  rge0srg  20388  zringunit  20407  znrrg  20484  psgnghm  20496  zrhpsgnevpm  20507  evpmodpmf1o  20512  pmtrodpm  20513  phlssphl  20575  frlmsslsp  20712  islinds4  20751  lmimlbs  20752  lbslcic  20757  psrbaglefi  20845  psrbaglefiOLD  20846  psrbagconf1o  20849  mplsubglem  20915  mplneg  20924  ressmpladd  20940  ressmplmul  20941  ressmplvsca  20942  mplmonmul  20947  ply1bascl  21078  mdetralt  21459  mdetunilem7  21469  chfacfpmmulgsum2  21716  tgval2  21807  ordtbas  22043  ordtrestixx  22073  hauslly  22343  kgentop  22393  ptbasin  22428  filunirn  22733  uzrest  22748  elflim  22822  flffval  22840  fclsval  22859  isfcls  22860  fcfval  22884  ustn0  23072  fmucndlem  23142  xmetunirn  23189  mopnval  23290  setsmstopn  23330  tmsval  23333  tngtopn  23502  qtopbaslem  23610  xrtgioo  23657  reperflem  23669  icccmplem1  23673  icopnfhmeo  23794  icccvx  23801  bndth  23809  reparphti  23848  pcoval1  23864  pcoval2  23867  pcoass  23875  pcorevlem  23877  pcorev2  23879  pi1xfrcnv  23908  csscld  24100  cfilfval  24115  caufval  24126  bcthlem1  24175  ivthlem1  24302  ivthlem3  24304  ovolicc2lem3  24370  ovolicc2lem4  24371  vitalilem1  24459  mbflimsup  24517  i1fd  24532  i1f0  24538  i1f1  24541  itg1addlem4  24550  itg1addlem4OLD  24551  itg1addlem5  24552  iblmbf  24619  ellimc2  24728  limcres  24737  limcun  24746  dvbsss  24753  perfdvf  24754  dvres2lem  24761  dvaddbr  24789  rolle  24841  cmvth  24842  dvlip  24844  dvlipcn  24845  dvle  24858  lhop1lem  24864  dvfsumle  24872  dvfsumge  24873  dvfsumabs  24874  dvfsumlem2  24878  ftc2  24895  itgparts  24898  itgsubstlem  24899  itgsubst  24900  deg1mul3  24967  coeval  25071  coeeu  25073  dgrval  25076  coef3  25080  coemulc  25103  dgrsub  25120  coecj  25126  dvply2  25133  dvnply  25135  quotval  25139  fta1  25155  plyexmo  25160  aacjcl  25174  taylfval  25205  dvtaylp  25216  abelth  25287  pilem3  25299  cos0pilt1  25375  sinord  25377  recosf1o  25378  resinf1o  25379  tanord1  25380  eff1olem  25391  dvloglem  25490  dvlog  25493  dvlog2lem  25494  advlogexp  25497  logtayl  25502  logtayl2  25504  dvcncxp1  25583  dvcnsqrt  25584  cxpcn3lem  25587  cxpcn3  25588  sqrtcn  25590  loglesqrt  25598  1cubr  25679  acosrecl  25740  efrlim  25806  jensen  25825  lgamgulmlem2  25866  lgamucov2  25875  basellem4  25920  musum  26027  dchrinvcl  26088  dchrghm  26091  dchrinv  26096  dchrsum2  26103  dchrsum  26104  rpvmasumlem  26322  dchrisum0lem2a  26352  pnt  26449  tglng  26591  axlowdimlem6  26992  axlowdimlem16  27002  axlowdimlem17  27003  axlowdim  27006  axeuclidlem  27007  axcontlem2  27010  axcontlem7  27015  axcontlem8  27016  nbusgrvtxm1uvtx  27447  wlk1walk  27680  pthdivtx  27770  pthdadjvtx  27771  crctcshwlkn0lem2  27849  crctcshwlkn0lem4  27851  clwwisshclwws  28052  fusgreg2wsp  28373  nvvcop  28629  nvex  28646  phnv  28849  sheli  29249  cheli  29267  hhssabloilem  29296  choc1  29362  shintcli  29364  chintcli  29366  shsleji  29405  pjini  29734  mayete3i  29763  dmadjop  29923  nlelshi  30095  cnlnadjeui  30112  cnlnssadj  30115  bdopadj  30117  pjimai  30211  stcl  30251  atelch  30379  fcnvgreu  30684  f1od2  30730  fcobijfs  30732  uzssico  30779  iundisj2fi  30792  nnindf  30807  eliccioo  30879  gsummptres  30985  cyc3genpm  31092  elrspunidl  31274  zarcls  31492  ordtrestNEW  31539  xrge0iifcnv  31551  xrge0iifcv  31552  xrge0iifiso  31553  xrge0iifhom  31555  qqhcn  31607  esumval  31680  gsumesum  31693  esumlub  31694  esumcst  31697  esumfsup  31704  issgon  31757  elrnsiga  31760  imambfm  31895  br2base  31902  sxbrsigalem0  31904  dya2iocucvr  31917  sxbrsigalem2  31919  sxbrsigalem5  31921  sxbrsiga  31923  omssubadd  31933  sitmcl  31984  oddpwdc  31987  eulerpartlemelr  31990  eulerpartlemgvv  32009  eulerpartlemgh  32011  eulerpartlemgs2  32013  eulerpartlemn  32014  sseqf  32025  ballotlem2  32121  ballotlemfp1  32124  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemfmpn  32127  ballotlemsup  32137  ballotlemfrceq  32161  signswch  32206  rpsqrtcn  32239  prodfzo03  32249  itgexpif  32252  bnj1533  32499  bnj1137  32642  bnj1286  32666  bnj1408  32683  bnj1417  32688  subfacp1lem5  32813  cvmsi  32894  gonar  33024  goalr  33026  mpst123  33169  mpstrcl  33170  msrrcl  33172  elmsta  33177  msubvrs  33189  elmpps  33202  elmthm  33205  bcprod  33373  dfon2lem4  33432  oldf  33727  leftirr  33759  rightirr  33760  lrold  33763  sltlpss  33773  pprodss4v  33872  ivthALT  34210  neibastop2lem  34235  nnssi2  34330  nnssi3  34331  bj-sngltagi  34858  bj-elid5  35024  bj-fvmptunsn1  35112  bj-smgrpssmgmel  35124  bj-mndsssmgrpel  35126  bj-cmnssmndel  35128  bj-grpssmndel  35130  bj-ablssgrpel  35132  bj-ablsscmnel  35134  bj-vecssmodel  35137  bj-rveccvec  35159  bj-rvecabl  35161  taupilemrplb  35174  icorempo  35208  elxp8  35228  sin2h  35453  cos2h  35454  tan2h  35455  poimirlem14  35477  poimirlem26  35489  poimirlem27  35490  poimirlem31  35494  poimirlem32  35495  mblfinlem1  35500  cnambfre  35511  dvtan  35513  itg2addnc  35517  itg2gt0cn  35518  ftc1cnnc  35535  ftc2nc  35545  dvasin  35547  dvacos  35548  cover2  35558  sstotbnd2  35618  heibor1lem  35653  heiborlem10  35664  opidonOLD  35696  exidcl  35720  rngosn3  35768  flddivrng  35843  toycom  36673  osumcllem7N  37662  pexmidlem4N  37673  diaintclN  38758  dibintclN  38867  mapd1o  39348  hdmapevec  39535  dvrelog2  39754  sticksstones1  39771  prjspvs  40098  prjspeclsp  40100  0prjspnrel  40113  elrfi  40160  elrfirn  40161  elrfirn2  40162  mrefg3  40174  diophin  40238  diophun  40239  eq0rabdioph  40242  eqrabdioph  40243  pellex  40301  rmxycomplete  40383  jm2.23  40462  aomclem2  40524  fglmod  40542  lsmfgcl  40543  lmhmfgima  40553  lmhmfgsplit  40555  isnumbasabl  40575  dgrsub2  40604  itgocn  40633  areaquad  40691  elmapintrab  40801  corcltrcl  40965  k0004val0  41382  elscottab  41476  radcnvrat  41546  uzmptshftfval  41578  binomcxplemdvsum  41587  binomcxplemnotnn0  41588  onfrALTlem2  41780  onfrALTlem2VD  42123  uzwo4  42215  mptssid  42398  uzublem  42584  eliccelioc  42675  elicores  42687  sqrlearg  42707  fsumiunss  42734  limcdm0  42777  sumnnodd  42789  fnlimfvre  42833  limsupubuzlem  42871  limsupmnflem  42879  limsupre3uzlem  42894  climuzlem  42902  cncfshift  43033  cncfperiod  43038  icccncfext  43046  dvnprodlem1  43105  dvnprodlem2  43106  itgsin0pilem1  43109  itgsinexplem1  43113  itgsinexp  43114  ditgeqiooicc  43119  itgsubsticclem  43134  itgioocnicc  43136  itgsbtaddcnst  43141  stoweidlem34  43193  stoweidlem41  43200  stoweidlem51  43210  wallispilem2  43225  stirlinglem11  43243  dirkercncflem2  43263  fourierdlem5  43271  fourierdlem9  43275  fourierdlem17  43283  fourierdlem18  43284  fourierdlem20  43286  fourierdlem39  43305  fourierdlem48  43313  fourierdlem49  43314  fourierdlem62  43327  fourierdlem66  43331  fourierdlem68  43333  fourierdlem72  43337  fourierdlem73  43338  fourierdlem81  43346  fourierdlem83  43348  fourierdlem85  43350  fourierdlem87  43352  fourierdlem88  43353  fourierdlem92  43357  fourierdlem95  43360  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  etransclem24  43417  etransclem35  43428  etransclem37  43430  salexct  43491  salgencntex  43500  sge0resplit  43562  sge0split  43565  meaiuninclem  43636  caratheodorylem1  43682  volicorescl  43709  hoidmv1lelem3  43749  opnvonmbllem2  43789  ovolval2  43800  ovolval3  43803  ovolval4lem1  43805  ovolval4lem2  43806  pimiooltgt  43863  sssmf  43889  smfaddlem1  43913  smflimlem2  43922  smfrec  43938  smfdiv  43946  smfsuplem1  43959  smfsuplem3  43961  fcores  44176  spr0el  44550  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbnd  44877  fldhmsubc  45258  fldhmsubcALTV  45276  fvconst0ci  45802  fvconstdomi  45803