Theorem sseli 3942

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3931

This theorem is referenced by:  sselii  3943  sselid  3944  elun1  4145  elun2  4146  elopabr  5521  elopabran  5522  elopaelxp  5728  copsex2ga  5770  2elresin  6639  nfvres  6899  fvco4i  6962  mptrcl  6977  fvmptss  6980  fvmptex  6982  fvmptnf  6990  elfvmptrab1w  6995  elfvmptrab1  6996  fvopab4ndm  6998  fvimacnvi  7024  elpreima  7030  iinpreima  7041  ofrfvalg  7661  ofval  7664  off  7671  nnon  7848  finds  7872  finds2  7874  eqopi  8004  op1steq  8012  dfoprab4  8034  bropopvvv  8069  bropfvvvv  8071  reldmtpos  8213  smores2  8323  frsuc  8405  unifpw  9306  cantnfp1lem1  9631  cantnfp1lem3  9633  r1fin  9726  r1tr  9729  r1ordg  9731  r1ord3g  9732  r1val1  9739  tz9.12lem3  9742  tcrank  9837  cplem1  9842  hta  9850  tskwe  9903  cardprclem  9932  alephfplem3  10059  dfac12r  10100  ackbij1lem16  10187  ackbij2  10195  fin23lem28  10293  fin23lem30  10295  fin23lem31  10296  fin1a2lem6  10358  hsmexlem4  10382  hsmexlem5  10383  hsmexlem6  10384  axdc2lem  10401  axdc3lem2  10404  axcclem  10410  brdom5  10482  brdom4  10483  r1tskina  10735  gruina  10771  grur1a  10772  pinn  10831  0nnq  10877  elpqn  10878  recn  11158  rexr  11220  ltord1  11704  leord1  11705  eqord1  11706  nnre  12193  nncn  12194  nnind  12204  nnnn0  12449  nn0re  12451  nn0cn  12452  nn0xnn0  12519  nnzOLD  12553  nn0z  12554  uzuzle35  12846  nnq  12921  qcn  12922  rpre  12960  eliccxr  13396  difreicc  13445  iccshftri  13448  iccshftli  13450  iccdili  13452  icccntri  13454  fzval2  13471  fzelp1  13537  4fvwrd4  13609  elfzo1  13673  ico01fl0  13781  expcllem  14037  expcl2lem  14038  m1expcl2  14050  bcm1k  14280  bcpasc  14286  hashbclem  14417  wrdv  14494  pfxfv0  14657  pfxfvlsw  14660  cshimadifsn  14795  swrds2m  14907  01sqrexlem5  15212  cau3lem  15321  caubnd  15325  climconst2  15514  o1of2  15579  o1rlimmul  15585  caurcvg  15643  caucvg  15645  binomlem  15795  incexclem  15802  divcnvshft  15821  zprod  15903  fprodge1  15961  risefaccllem  15979  fallfaccllem  15980  bpolydiflem  16020  bpoly4  16025  dvdsflip  16287  divalglem8  16370  sadadd  16437  smumul  16463  isprm3  16653  phimullem  16749  prmdiveq  16756  unbenlem  16879  vdwnnlem1  16966  vdwnnlem3  16968  ramtcl2  16982  prmgaplem4  17025  cshwshashlem1  17066  structcnvcnv  17123  fvsetsid  17138  imasdsval2  17479  mreunirn  17562  mrcfval  17569  mrisval  17591  coapm  18033  tsrss  18548  submnd0  18690  smndex1id  18838  nmzsubg  19097  nmznsg  19100  cntzmhm  19273  symgtrinv  19402  pmtrdifellem4  19409  psgnpmtr  19440  efginvrel2  19657  efginvrel1  19658  efgsp1  19667  efgsres  19668  efgsfo  19669  frgpinv  19694  frgpupf  19703  frgpup1  19705  subcmn  19767  torsubg  19784  dprd2dlem1  19973  dpjidcl  19990  ablfaclem3  20019  nzrring  20425  lringnzr  20450  fldhmsubc  20694  acsfn1p  20708  lssacs  20873  cnsubdrglem  21335  rege0subm  21340  rge0srg  21355  zringunit  21376  znrrg  21475  psgnghm  21489  zrhpsgnevpm  21500  evpmodpmf1o  21505  pmtrodpm  21506  phlssphl  21568  frlmsslsp  21705  islinds4  21744  lmimlbs  21745  lbslcic  21750  psrbaglefi  21835  psrbagconf1o  21838  mplsubglem  21908  mplneg  21919  ressmpladd  21936  ressmplmul  21937  ressmplvsca  21938  mplmonmul  21943  psdmul  22053  ply1bascl  22088  mdetralt  22495  mdetunilem7  22505  chfacfpmmulgsum2  22752  tgval2  22843  ordtbas  23079  ordtrestixx  23109  hauslly  23379  kgentop  23429  ptbasin  23464  filunirn  23769  uzrest  23784  elflim  23858  flffval  23876  fclsval  23895  isfcls  23896  fcfval  23920  ustn0  24108  fmucndlem  24178  xmetunirn  24225  mopnval  24326  setsmstopn  24366  tmsval  24369  tngtopn  24538  qtopbaslem  24646  xrtgioo  24695  reperflem  24707  icccmplem1  24711  icopnfhmeo  24841  icccvx  24848  bndth  24857  reparphtiOLD  24897  pcoval1  24913  pcoval2  24916  pcoass  24924  pcorevlem  24926  pcorev2  24928  pi1xfrcnv  24957  csscld  25149  cfilfval  25164  caufval  25175  bcthlem1  25224  ivthlem1  25352  ivthlem3  25354  ovolicc2lem3  25420  ovolicc2lem4  25421  vitalilem1  25509  mbflimsup  25567  i1fd  25582  i1f0  25588  i1f1  25591  itg1addlem4  25600  itg1addlem5  25601  iblmbf  25668  ellimc2  25778  limcres  25787  limcun  25796  dvbsss  25803  perfdvf  25804  dvres2lem  25811  dvaddbr  25840  rolle  25894  cmvth  25895  cmvthOLD  25896  dvlip  25898  dvlipcn  25899  dvle  25912  lhop1lem  25918  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc2  25951  itgparts  25954  itgsubstlem  25955  itgsubst  25956  deg1mul3  26021  coeval  26128  coeeu  26130  dgrval  26133  coef3  26137  coemulc  26160  dgrsub  26178  coecj  26184  coecjOLD  26186  dvply2  26194  dvnply  26196  quotval  26200  fta1  26216  plyexmo  26221  aacjcl  26235  taylfval  26266  dvtaylp  26278  abelth  26351  pilem3  26363  cos0pilt1  26441  sinord  26443  recosf1o  26444  resinf1o  26445  tanord1  26446  eff1olem  26457  dvloglem  26557  dvlog  26560  dvlog2lem  26561  advlogexp  26564  logtayl  26569  logtayl2  26571  dvcncxp1  26652  dvcnsqrt  26653  cxpcn3lem  26657  cxpcn3  26658  sqrtcn  26660  loglesqrt  26671  1cubr  26752  acosrecl  26813  efrlim  26879  efrlimOLD  26880  jensen  26899  lgamgulmlem2  26940  lgamucov2  26949  basellem4  26994  musum  27101  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dchrinvcl  27164  dchrghm  27167  dchrinv  27172  dchrsum2  27179  dchrsum  27180  rpvmasumlem  27398  dchrisum0lem2a  27428  pnt  27525  oldf  27765  leftirr  27802  rightirr  27803  lrold  27808  newbdayim  27814  sltlpss  27819  addsproplem2  27877  sleadd1  27896  addsuniflem  27908  addsbdaylem  27923  addsbday  27924  negsproplem2  27935  negsid  27947  negsunif  27961  mulsrid  28016  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  precsexlem9  28117  precsexlem11  28119  onsno  28156  onscutlt  28165  onaddscl  28174  onmulscl  28175  n0sno  28216  nnsno  28217  nnn0s  28220  nnsgt0  28231  zno  28270  expscllem  28316  tglng  28473  axlowdimlem6  28874  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  axeuclidlem  28889  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  nbusgrvtxm1uvtx  29332  wlk1walk  29567  pthdivtx  29657  pthdadjvtx  29658  crctcshwlkn0lem2  29741  crctcshwlkn0lem4  29743  clwwisshclwws  29944  fusgreg2wsp  30265  nvvcop  30523  nvex  30540  phnv  30743  sheli  31143  cheli  31161  hhssabloilem  31190  choc1  31256  shintcli  31258  chintcli  31260  shsleji  31299  pjini  31628  mayete3i  31657  dmadjop  31817  nlelshi  31989  cnlnadjeui  32006  cnlnssadj  32009  bdopadj  32011  pjimai  32105  stcl  32145  atelch  32273  fcnvgreu  32597  f1od2  32644  fcobijfs  32646  uzssico  32707  iundisj2fi  32720  nnindf  32744  eliccioo  32851  gsummptres  32992  cyc3genpm  33109  elrspunidl  33399  zarcls  33864  ordtrestNEW  33911  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iifiso  33925  xrge0iifhom  33927  qqhcn  33981  esumval  34036  gsumesum  34049  esumlub  34050  esumcst  34053  esumfsup  34060  issgon  34113  elrnsiga  34116  imambfm  34253  br2base  34260  sxbrsigalem0  34262  dya2iocucvr  34275  sxbrsigalem2  34277  sxbrsigalem5  34279  sxbrsiga  34281  omssubadd  34291  sitmcl  34342  oddpwdc  34345  eulerpartlemelr  34348  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemgs2  34371  eulerpartlemn  34372  sseqf  34383  ballotlem2  34480  ballotlemfp1  34483  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemfmpn  34486  ballotlemsup  34496  ballotlemfrceq  34520  signswch  34552  rpsqrtcn  34584  prodfzo03  34594  itgexpif  34597  bnj1533  34842  bnj1137  34985  bnj1286  35009  bnj1408  35026  bnj1417  35031  onvf1odlem4  35093  subfacp1lem5  35171  cvmsi  35252  gonar  35382  goalr  35384  mpst123  35527  mpstrcl  35528  msrrcl  35530  elmsta  35535  msubvrs  35547  elmpps  35560  elmthm  35563  bcprod  35725  dfon2lem4  35774  pprodss4v  35872  ivthALT  36323  neibastop2lem  36348  nnssi2  36443  nnssi3  36444  bj-sngltagi  36970  bj-elid5  37157  bj-fvmptunsn1  37245  bj-smgrpssmgmel  37257  bj-mndsssmgrpel  37259  bj-cmnssmndel  37261  bj-grpssmndel  37263  bj-ablssgrpel  37265  bj-ablsscmnel  37267  bj-vecssmodel  37270  bj-flddrng  37277  bj-rveccvec  37293  bj-rvecabl  37295  taupilemrplb  37308  icorempo  37339  elxp8  37359  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem14  37628  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  mblfinlem1  37651  cnambfre  37662  dvtan  37664  itg2addnc  37668  itg2gt0cn  37669  ftc1cnnc  37686  ftc2nc  37696  dvasin  37698  dvacos  37699  cover2  37709  sstotbnd2  37768  heibor1lem  37803  heiborlem10  37814  opidonOLD  37846  exidcl  37870  rngosn3  37918  flddivrng  37993  toycom  38966  osumcllem7N  39956  pexmidlem4N  39967  diaintclN  41052  dibintclN  41161  mapd1o  41642  hdmapevec  41829  dvrelog2  42052  aks6d1c2lem4  42115  sticksstones1  42134  aks6d1c6lem5  42165  redvmptabs  42348  imacrhmcl  42502  prjspvs  42598  prjspeclsp  42600  0prjspnrel  42615  elrfi  42682  elrfirn  42683  elrfirn2  42684  mrefg3  42696  diophin  42760  diophun  42761  eq0rabdioph  42764  eqrabdioph  42765  pellex  42823  rmxycomplete  42906  jm2.23  42985  aomclem2  43044  fglmod  43062  lsmfgcl  43063  lmhmfgima  43073  lmhmfgsplit  43075  isnumbasabl  43095  dgrsub2  43124  itgocn  43153  areaquad  43205  cantnftermord  43309  omabs2  43321  nna1iscard  43534  elmapintrab  43565  corcltrcl  43728  k0004val0  44143  elscottab  44233  radcnvrat  44303  uzmptshftfval  44335  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  onfrALTlem2  44536  onfrALTlem2VD  44878  uzwo4  45047  mptssid  45235  uzublem  45426  eliccelioc  45519  elicores  45531  sqrlearg  45551  fsumiunss  45573  limcdm0  45616  sumnnodd  45628  fnlimfvre  45672  limsupubuzlem  45710  limsupmnflem  45718  limsupre3uzlem  45733  climuzlem  45741  liminflelimsuplem  45773  cncfshift  45872  cncfperiod  45877  icccncfext  45885  dvnprodlem1  45944  dvnprodlem2  45945  itgsin0pilem1  45948  itgsinexplem1  45952  itgsinexp  45953  ditgeqiooicc  45958  itgsubsticclem  45973  itgioocnicc  45975  itgsbtaddcnst  45980  stoweidlem34  46032  stoweidlem41  46039  stoweidlem51  46049  wallispilem2  46064  stirlinglem11  46082  dirkercncflem2  46102  fourierdlem5  46110  fourierdlem9  46114  fourierdlem17  46122  fourierdlem18  46123  fourierdlem20  46125  fourierdlem39  46144  fourierdlem48  46152  fourierdlem49  46153  fourierdlem62  46166  fourierdlem66  46170  fourierdlem68  46172  fourierdlem72  46176  fourierdlem73  46177  fourierdlem81  46185  fourierdlem83  46187  fourierdlem85  46189  fourierdlem87  46191  fourierdlem88  46192  fourierdlem92  46196  fourierdlem95  46199  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  etransclem24  46256  etransclem35  46267  etransclem37  46269  salexct  46332  salgencntex  46341  sge0resplit  46404  sge0split  46407  meaiuninclem  46478  caratheodorylem1  46524  volicorescl  46551  hoidmv1lelem3  46591  opnvonmbllem2  46631  ovolval2  46642  ovolval3  46645  ovolval4lem1  46647  ovolval4lem2  46648  pimiooltgt  46708  sssmf  46736  smfaddlem1  46761  smflimlem2  46770  smfrec  46787  smfdiv  46795  smfsuplem1  46809  smfsuplem3  46811  et-ltneverrefl  46869  natglobalincr  46875  tannpoly  46891  fcores  47068  rehalfge1  47336  spr0el  47483  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  upgrimpthslem2  47908  stgredgiun  47957  isubgr3stgrlem7  47971  fldhmsubcALTV  48321  fvconst0ci  48879  fvconstdomi  48880  idfullsubc  49150  fulloppf  49152  fthoppf  49153  initopropdlemlem  49228