Theorem sseli 3927

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2809  df-ss 3916

This theorem is referenced by:  sselii  3928  sselid  3929  elun1  4132  elun2  4133  elopabr  5506  elopabran  5507  elopaelxp  5712  copsex2ga  5754  2elresin  6611  nfvres  6870  fvco4i  6933  mptrcl  6948  fvmptss  6951  fvmptex  6953  fvmptnf  6961  elfvmptrab1w  6966  elfvmptrab1  6967  fvopab4ndm  6969  fvimacnvi  6995  elpreima  7001  iinpreima  7012  ofrfvalg  7628  ofval  7631  off  7638  nnon  7812  finds  7836  finds2  7838  eqopi  7967  op1steq  7975  dfoprab4  7997  bropopvvv  8030  bropfvvvv  8032  reldmtpos  8174  smores2  8284  frsuc  8366  unifpw  9253  cantnfp1lem1  9585  cantnfp1lem3  9587  r1fin  9683  r1tr  9686  r1ordg  9688  r1ord3g  9689  r1val1  9696  tz9.12lem3  9699  tcrank  9794  cplem1  9799  hta  9807  tskwe  9860  cardprclem  9889  alephfplem3  10014  dfac12r  10055  ackbij1lem16  10142  ackbij2  10150  fin23lem28  10248  fin23lem30  10250  fin23lem31  10251  fin1a2lem6  10313  hsmexlem4  10337  hsmexlem5  10338  hsmexlem6  10339  axdc2lem  10356  axdc3lem2  10359  axcclem  10365  brdom5  10437  brdom4  10438  r1tskina  10691  gruina  10727  grur1a  10728  pinn  10787  0nnq  10833  elpqn  10834  recn  11114  rexr  11176  ltord1  11661  leord1  11662  eqord1  11663  nnre  12150  nncn  12151  nnind  12161  nnnn0  12406  nn0re  12408  nn0cn  12409  nn0xnn0  12476  nn0z  12510  uzuzle35  12798  nnq  12873  qcn  12874  rpre  12912  eliccxr  13349  difreicc  13398  iccshftri  13401  iccshftli  13403  iccdili  13405  icccntri  13407  fzval2  13424  fzelp1  13490  4fvwrd4  13562  elfzo1  13626  ico01fl0  13737  expcllem  13993  expcl2lem  13994  m1expcl2  14006  bcm1k  14236  bcpasc  14242  hashbclem  14373  wrdv  14450  pfxfv0  14613  pfxfvlsw  14616  cshimadifsn  14750  swrds2m  14862  01sqrexlem5  15167  cau3lem  15276  caubnd  15280  climconst2  15469  o1of2  15534  o1rlimmul  15540  caurcvg  15598  caucvg  15600  binomlem  15750  incexclem  15757  divcnvshft  15776  zprod  15858  fprodge1  15916  risefaccllem  15934  fallfaccllem  15935  bpolydiflem  15975  bpoly4  15980  dvdsflip  16242  divalglem8  16325  sadadd  16392  smumul  16418  isprm3  16608  phimullem  16704  prmdiveq  16711  unbenlem  16834  vdwnnlem1  16921  vdwnnlem3  16923  ramtcl2  16937  prmgaplem4  16980  cshwshashlem1  17021  structcnvcnv  17078  fvsetsid  17093  imasdsval2  17435  mreunirn  17518  mrcfval  17529  mrisval  17551  coapm  17993  tsrss  18510  chnccat  18547  ex-chn1  18558  submnd0  18686  smndex1id  18834  nmzsubg  19092  nmznsg  19095  cntzmhm  19268  symgtrinv  19399  pmtrdifellem4  19406  psgnpmtr  19437  efginvrel2  19654  efginvrel1  19655  efgsp1  19664  efgsres  19665  efgsfo  19666  frgpinv  19691  frgpupf  19700  frgpup1  19702  subcmn  19764  torsubg  19781  dprd2dlem1  19970  dpjidcl  19987  ablfaclem3  20016  nzrring  20447  lringnzr  20472  fldhmsubc  20716  acsfn1p  20730  lssacs  20916  cnsubdrglem  21371  rege0subm  21376  rge0srg  21391  zringunit  21419  znrrg  21518  psgnghm  21533  zrhpsgnevpm  21544  evpmodpmf1o  21549  pmtrodpm  21550  phlssphl  21612  frlmsslsp  21749  islinds4  21788  lmimlbs  21789  lbslcic  21794  psrbaglefi  21880  psrbagconf1o  21883  mplsubglem  21952  mplneg  21963  ressmpladd  21982  ressmplmul  21983  ressmplvsca  21984  mplmonmul  21989  psdmul  22107  ply1bascl  22142  mdetralt  22550  mdetunilem7  22560  chfacfpmmulgsum2  22807  tgval2  22898  ordtbas  23134  ordtrestixx  23164  hauslly  23434  kgentop  23484  ptbasin  23519  filunirn  23824  uzrest  23839  elflim  23913  flffval  23931  fclsval  23950  isfcls  23951  fcfval  23975  ustn0  24163  fmucndlem  24232  xmetunirn  24279  mopnval  24380  setsmstopn  24420  tmsval  24423  tngtopn  24592  qtopbaslem  24700  xrtgioo  24749  reperflem  24761  icccmplem1  24765  icopnfhmeo  24895  icccvx  24902  bndth  24911  reparphtiOLD  24951  pcoval1  24967  pcoval2  24970  pcoass  24978  pcorevlem  24980  pcorev2  24982  pi1xfrcnv  25011  csscld  25203  cfilfval  25218  caufval  25229  bcthlem1  25278  ivthlem1  25406  ivthlem3  25408  ovolicc2lem3  25474  ovolicc2lem4  25475  vitalilem1  25563  mbflimsup  25621  i1fd  25636  i1f0  25642  i1f1  25645  itg1addlem4  25654  itg1addlem5  25655  iblmbf  25722  ellimc2  25832  limcres  25841  limcun  25850  dvbsss  25857  perfdvf  25858  dvres2lem  25865  dvaddbr  25894  rolle  25948  cmvth  25949  cmvthOLD  25950  dvlip  25952  dvlipcn  25953  dvle  25966  lhop1lem  25972  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  dvfsumlem2  25987  dvfsumlem2OLD  25988  ftc2  26005  itgparts  26008  itgsubstlem  26009  itgsubst  26010  deg1mul3  26075  coeval  26182  coeeu  26184  dgrval  26187  coef3  26191  coemulc  26214  dgrsub  26232  coecj  26238  coecjOLD  26240  dvply2  26248  dvnply  26250  quotval  26254  fta1  26270  plyexmo  26275  aacjcl  26289  taylfval  26320  dvtaylp  26332  abelth  26405  pilem3  26417  cos0pilt1  26495  sinord  26497  recosf1o  26498  resinf1o  26499  tanord1  26500  eff1olem  26511  dvloglem  26611  dvlog  26614  dvlog2lem  26615  advlogexp  26618  logtayl  26623  logtayl2  26625  dvcncxp1  26706  dvcnsqrt  26707  cxpcn3lem  26711  cxpcn3  26712  sqrtcn  26714  loglesqrt  26725  1cubr  26806  acosrecl  26867  efrlim  26933  efrlimOLD  26934  jensen  26953  lgamgulmlem2  26994  lgamucov2  27003  basellem4  27048  musum  27155  mpodvdsmulf1o  27158  fsumdvdsmul  27159  dchrinvcl  27218  dchrghm  27221  dchrinv  27226  dchrsum2  27233  dchrsum  27234  rpvmasumlem  27452  dchrisum0lem2a  27482  pnt  27579  oldf  27825  leftirr  27863  rightirr  27864  lrold  27869  newbdayim  27875  sltlpss  27880  addsproplem2  27940  sleadd1  27959  addsuniflem  27971  addsbdaylem  27986  addsbday  27987  negsproplem2  27998  negsid  28010  negsunif  28024  negsleft  28027  negsright  28028  mulsrid  28082  mulsproplem12  28096  mulsproplem13  28097  mulsproplem14  28098  precsexlem9  28183  precsexlem11  28185  onsno  28223  onscutlt  28232  onaddscl  28241  onmulscl  28242  n0sno  28284  nnsno  28285  nnn0s  28288  nnsgt0  28299  zno  28340  expscllem  28388  elreno2  28440  tglng  28567  axlowdimlem6  28969  axlowdimlem16  28979  axlowdimlem17  28980  axlowdim  28983  axeuclidlem  28984  axcontlem2  28987  axcontlem7  28992  axcontlem8  28993  nbusgrvtxm1uvtx  29427  wlk1walk  29661  pthdivtx  29749  pthdadjvtx  29750  crctcshwlkn0lem2  29833  crctcshwlkn0lem4  29835  clwwisshclwws  30039  fusgreg2wsp  30360  nvvcop  30618  nvex  30635  phnv  30838  sheli  31238  cheli  31256  hhssabloilem  31285  choc1  31351  shintcli  31353  chintcli  31355  shsleji  31394  pjini  31723  mayete3i  31752  dmadjop  31912  nlelshi  32084  cnlnadjeui  32101  cnlnssadj  32104  bdopadj  32106  pjimai  32200  stcl  32240  atelch  32368  fcnvgreu  32700  f1od2  32747  fcobijfs  32749  fcobijfs2  32750  uzssico  32813  iundisj2fi  32826  nnindf  32849  eliccioo  32961  gsummptres  33084  cyc3genpm  33183  elrspunidl  33458  zarcls  33980  ordtrestNEW  34027  xrge0iifcnv  34039  xrge0iifcv  34040  xrge0iifiso  34041  xrge0iifhom  34043  qqhcn  34097  esumval  34152  gsumesum  34165  esumlub  34166  esumcst  34169  esumfsup  34176  issgon  34229  elrnsiga  34232  imambfm  34368  br2base  34375  sxbrsigalem0  34377  dya2iocucvr  34390  sxbrsigalem2  34392  sxbrsigalem5  34394  sxbrsiga  34396  omssubadd  34406  sitmcl  34457  oddpwdc  34460  eulerpartlemelr  34463  eulerpartlemgvv  34482  eulerpartlemgh  34484  eulerpartlemgs2  34486  eulerpartlemn  34487  sseqf  34498  ballotlem2  34595  ballotlemfp1  34598  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemfmpn  34601  ballotlemsup  34611  ballotlemfrceq  34635  signswch  34667  rpsqrtcn  34699  prodfzo03  34709  itgexpif  34712  bnj1533  34957  bnj1137  35100  bnj1286  35124  bnj1408  35141  bnj1417  35146  r1omhf  35211  onvf1odlem4  35249  subfacp1lem5  35327  cvmsi  35408  gonar  35538  goalr  35540  mpst123  35683  mpstrcl  35684  msrrcl  35686  elmsta  35691  msubvrs  35703  elmpps  35716  elmthm  35719  bcprod  35881  dfon2lem4  35927  pprodss4v  36025  ivthALT  36478  neibastop2lem  36503  nnssi2  36598  nnssi3  36599  bj-sngltagi  37126  bj-elid5  37313  bj-fvmptunsn1  37401  bj-smgrpssmgmel  37413  bj-mndsssmgrpel  37415  bj-cmnssmndel  37417  bj-grpssmndel  37419  bj-ablssgrpel  37421  bj-ablsscmnel  37423  bj-vecssmodel  37426  bj-flddrng  37433  bj-rveccvec  37449  bj-rvecabl  37451  taupilemrplb  37464  icorempo  37495  elxp8  37515  sin2h  37750  cos2h  37751  tan2h  37752  poimirlem14  37774  poimirlem26  37786  poimirlem27  37787  poimirlem31  37791  poimirlem32  37792  mblfinlem1  37797  cnambfre  37808  dvtan  37810  itg2addnc  37814  itg2gt0cn  37815  ftc1cnnc  37832  ftc2nc  37842  dvasin  37844  dvacos  37845  cover2  37855  sstotbnd2  37914  heibor1lem  37949  heiborlem10  37960  opidonOLD  37992  exidcl  38016  rngosn3  38064  flddivrng  38139  toycom  39172  osumcllem7N  40161  pexmidlem4N  40172  diaintclN  41257  dibintclN  41366  mapd1o  41847  hdmapevec  42034  dvrelog2  42257  aks6d1c2lem4  42320  sticksstones1  42339  aks6d1c6lem5  42370  redvmptabs  42557  imacrhmcl  42711  prjspvs  42795  prjspeclsp  42797  0prjspnrel  42812  elrfi  42878  elrfirn  42879  elrfirn2  42880  mrefg3  42892  diophin  42956  diophun  42957  eq0rabdioph  42960  eqrabdioph  42961  pellex  43019  rmxycomplete  43101  jm2.23  43180  aomclem2  43239  fglmod  43257  lsmfgcl  43258  lmhmfgima  43268  lmhmfgsplit  43270  isnumbasabl  43290  dgrsub2  43319  itgocn  43348  areaquad  43400  cantnftermord  43504  omabs2  43516  nna1iscard  43728  elmapintrab  43759  corcltrcl  43922  k0004val0  44337  elscottab  44427  radcnvrat  44497  uzmptshftfval  44529  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  onfrALTlem2  44729  onfrALTlem2VD  45071  uzwo4  45240  mptssid  45427  uzublem  45616  eliccelioc  45709  elicores  45721  sqrlearg  45741  fsumiunss  45763  limcdm0  45806  sumnnodd  45818  fnlimfvre  45860  limsupubuzlem  45898  limsupmnflem  45906  limsupre3uzlem  45921  climuzlem  45929  liminflelimsuplem  45961  cncfshift  46060  cncfperiod  46065  icccncfext  46073  dvnprodlem1  46132  dvnprodlem2  46133  itgsin0pilem1  46136  itgsinexplem1  46140  itgsinexp  46141  ditgeqiooicc  46146  itgsubsticclem  46161  itgioocnicc  46163  itgsbtaddcnst  46168  stoweidlem34  46220  stoweidlem41  46227  stoweidlem51  46237  wallispilem2  46252  stirlinglem11  46270  dirkercncflem2  46290  fourierdlem5  46298  fourierdlem9  46302  fourierdlem17  46310  fourierdlem18  46311  fourierdlem20  46313  fourierdlem39  46332  fourierdlem48  46340  fourierdlem49  46341  fourierdlem62  46354  fourierdlem66  46358  fourierdlem68  46360  fourierdlem72  46364  fourierdlem73  46365  fourierdlem81  46373  fourierdlem83  46375  fourierdlem85  46377  fourierdlem87  46379  fourierdlem88  46380  fourierdlem92  46384  fourierdlem95  46387  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  sqwvfoura  46414  sqwvfourb  46415  fouriersw  46417  etransclem24  46444  etransclem35  46455  etransclem37  46457  salexct  46520  salgencntex  46529  sge0resplit  46592  sge0split  46595  meaiuninclem  46666  caratheodorylem1  46712  volicorescl  46739  hoidmv1lelem3  46779  opnvonmbllem2  46819  ovolval2  46830  ovolval3  46833  ovolval4lem1  46835  ovolval4lem2  46836  sssmf  46924  smfaddlem1  46949  smflimlem2  46958  smfrec  46975  smfdiv  46983  smfsuplem1  46997  smfsuplem3  46999  et-ltneverrefl  47057  natglobalincr  47063  tannpoly  47078  fcores  47255  rehalfge1  47523  spr0el  47670  bgoldbtbndlem2  47994  bgoldbtbndlem3  47995  bgoldbtbnd  47997  upgrimpthslem2  48096  stgredgiun  48146  isubgr3stgrlem7  48160  fldhmsubcALTV  48521  fvconst0ci  49078  fvconstdomi  49079  idfullsubc  49348  fulloppf  49350  fthoppf  49351  initopropdlemlem  49426