Theorem sseli 3918

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sselii  3919  sselid  3920  elun1  4111  elun2  4112  elopabr  5475  elopabran  5476  elopaelxp  5677  copsex2ga  5719  2elresin  6562  nfvres  6819  fvco4i  6878  mptrcl  6893  fvmptss  6896  fvmptex  6898  fvmptnf  6906  elfvmptrab1w  6910  elfvmptrab1  6911  fvopab4ndm  6913  fvimacnvi  6938  elpreima  6944  iinpreima  6955  ofrfvalg  7550  ofval  7553  off  7560  nnon  7727  finds  7754  finds2  7756  eqopi  7876  op1steq  7884  dfoprab4  7904  bropopvvv  7939  bropfvvvv  7941  reldmtpos  8059  wfrlem10OLD  8158  smores2  8194  frsuc  8277  nnfiOLD  9024  unifpw  9131  cantnfp1lem1  9445  cantnfp1lem3  9447  r1fin  9540  r1tr  9543  r1ordg  9545  r1ord3g  9546  r1val1  9553  tz9.12lem3  9556  tcrank  9651  cplem1  9656  hta  9664  tskwe  9717  cardprclem  9746  alephfplem3  9871  dfac12r  9911  ackbij1lem16  10000  ackbij2  10008  fin23lem28  10105  fin23lem30  10107  fin23lem31  10108  fin1a2lem6  10170  hsmexlem4  10194  hsmexlem5  10195  hsmexlem6  10196  axdc2lem  10213  axdc3lem2  10216  axcclem  10222  brdom5  10294  brdom4  10295  r1tskina  10547  gruina  10583  grur1a  10584  pinn  10643  0nnq  10689  elpqn  10690  recn  10970  rexr  11030  ltord1  11510  leord1  11511  eqord1  11512  nnre  11989  nncn  11990  nnind  12000  nnnn0  12249  nn0re  12251  nn0cn  12252  nn0xnn0  12318  nnz  12351  nn0z  12352  nnq  12711  qcn  12712  rpre  12747  eliccxr  13176  difreicc  13225  iccshftri  13228  iccshftli  13230  iccdili  13232  icccntri  13234  fzval2  13251  fzelp1  13317  4fvwrd4  13385  elfzo1  13446  ico01fl0  13548  expcllem  13802  expcl2lem  13803  m1expcl2  13813  bcm1k  14038  bcpasc  14044  hashbclem  14173  wrdv  14241  pfxfv0  14414  pfxfvlsw  14417  cshimadifsn  14551  swrds2m  14663  sqrlem5  14967  cau3lem  15075  caubnd  15079  climconst2  15266  o1of2  15331  o1rlimmul  15337  caurcvg  15397  caucvg  15399  binomlem  15550  incexclem  15557  divcnvshft  15576  zprod  15656  fprodge1  15714  risefaccllem  15732  fallfaccllem  15733  bpolydiflem  15773  bpoly4  15778  dvdsflip  16035  divalglem8  16118  sadadd  16183  smumul  16209  isprm3  16397  phimullem  16489  prmdiveq  16496  unbenlem  16618  vdwnnlem1  16705  vdwnnlem3  16707  ramtcl2  16721  prmgaplem4  16764  cshwshashlem1  16806  structcnvcnv  16863  fvsetsid  16878  imasdsval2  17236  mreunirn  17319  mrcfval  17326  mrisval  17348  coapm  17795  tsrss  18316  submnd0  18423  smndex1id  18559  nmzsubg  18802  nmznsg  18805  cntzmhm  18954  symgtrinv  19089  pmtrdifellem4  19096  psgnpmtr  19127  efginvrel2  19342  efginvrel1  19343  efgsp1  19352  efgsres  19353  efgsfo  19354  frgpinv  19379  frgpupf  19388  frgpup1  19390  subcmn  19447  torsubg  19464  dprd2dlem1  19653  dpjidcl  19670  ablfaclem3  19699  acsfn1p  20076  lssacs  20238  cnsubdrglem  20658  rege0subm  20663  rge0srg  20678  zringunit  20697  znrrg  20782  psgnghm  20794  zrhpsgnevpm  20805  evpmodpmf1o  20810  pmtrodpm  20811  phlssphl  20873  frlmsslsp  21012  islinds4  21051  lmimlbs  21052  lbslcic  21057  psrbaglefi  21144  psrbaglefiOLD  21145  psrbagconf1o  21148  mplsubglem  21214  mplneg  21223  ressmpladd  21239  ressmplmul  21240  ressmplvsca  21241  mplmonmul  21246  ply1bascl  21383  mdetralt  21766  mdetunilem7  21776  chfacfpmmulgsum2  22023  tgval2  22115  ordtbas  22352  ordtrestixx  22382  hauslly  22652  kgentop  22702  ptbasin  22737  filunirn  23042  uzrest  23057  elflim  23131  flffval  23149  fclsval  23168  isfcls  23169  fcfval  23193  ustn0  23381  fmucndlem  23452  xmetunirn  23499  mopnval  23600  setsmstopn  23642  tmsval  23645  tngtopn  23823  qtopbaslem  23931  xrtgioo  23978  reperflem  23990  icccmplem1  23994  icopnfhmeo  24115  icccvx  24122  bndth  24130  reparphti  24169  pcoval1  24185  pcoval2  24188  pcoass  24196  pcorevlem  24198  pcorev2  24200  pi1xfrcnv  24229  csscld  24422  cfilfval  24437  caufval  24448  bcthlem1  24497  ivthlem1  24624  ivthlem3  24626  ovolicc2lem3  24692  ovolicc2lem4  24693  vitalilem1  24781  mbflimsup  24839  i1fd  24854  i1f0  24860  i1f1  24863  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  iblmbf  24941  ellimc2  25050  limcres  25059  limcun  25068  dvbsss  25075  perfdvf  25076  dvres2lem  25083  dvaddbr  25111  rolle  25163  cmvth  25164  dvlip  25166  dvlipcn  25167  dvle  25180  lhop1lem  25186  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem2  25200  ftc2  25217  itgparts  25220  itgsubstlem  25221  itgsubst  25222  deg1mul3  25289  coeval  25393  coeeu  25395  dgrval  25398  coef3  25402  coemulc  25425  dgrsub  25442  coecj  25448  dvply2  25455  dvnply  25457  quotval  25461  fta1  25477  plyexmo  25482  aacjcl  25496  taylfval  25527  dvtaylp  25538  abelth  25609  pilem3  25621  cos0pilt1  25697  sinord  25699  recosf1o  25700  resinf1o  25701  tanord1  25702  eff1olem  25713  dvloglem  25812  dvlog  25815  dvlog2lem  25816  advlogexp  25819  logtayl  25824  logtayl2  25826  dvcncxp1  25905  dvcnsqrt  25906  cxpcn3lem  25909  cxpcn3  25910  sqrtcn  25912  loglesqrt  25920  1cubr  26001  acosrecl  26062  efrlim  26128  jensen  26147  lgamgulmlem2  26188  lgamucov2  26197  basellem4  26242  musum  26349  dchrinvcl  26410  dchrghm  26413  dchrinv  26418  dchrsum2  26425  dchrsum  26426  rpvmasumlem  26644  dchrisum0lem2a  26674  pnt  26771  tglng  26916  axlowdimlem6  27324  axlowdimlem16  27334  axlowdimlem17  27335  axlowdim  27338  axeuclidlem  27339  axcontlem2  27342  axcontlem7  27347  axcontlem8  27348  nbusgrvtxm1uvtx  27781  wlk1walk  28015  pthdivtx  28106  pthdadjvtx  28107  crctcshwlkn0lem2  28185  crctcshwlkn0lem4  28187  clwwisshclwws  28388  fusgreg2wsp  28709  nvvcop  28965  nvex  28982  phnv  29185  sheli  29585  cheli  29603  hhssabloilem  29632  choc1  29698  shintcli  29700  chintcli  29702  shsleji  29741  pjini  30070  mayete3i  30099  dmadjop  30259  nlelshi  30431  cnlnadjeui  30448  cnlnssadj  30451  bdopadj  30453  pjimai  30547  stcl  30587  atelch  30715  fcnvgreu  31019  f1od2  31065  fcobijfs  31067  uzssico  31114  iundisj2fi  31127  nnindf  31142  eliccioo  31214  gsummptres  31321  cyc3genpm  31428  elrspunidl  31615  zarcls  31833  ordtrestNEW  31880  xrge0iifcnv  31892  xrge0iifcv  31893  xrge0iifiso  31894  xrge0iifhom  31896  qqhcn  31950  esumval  32023  gsumesum  32036  esumlub  32037  esumcst  32040  esumfsup  32047  issgon  32100  elrnsiga  32103  imambfm  32238  br2base  32245  sxbrsigalem0  32247  dya2iocucvr  32260  sxbrsigalem2  32262  sxbrsigalem5  32264  sxbrsiga  32266  omssubadd  32276  sitmcl  32327  oddpwdc  32330  eulerpartlemelr  32333  eulerpartlemgvv  32352  eulerpartlemgh  32354  eulerpartlemgs2  32356  eulerpartlemn  32357  sseqf  32368  ballotlem2  32464  ballotlemfp1  32467  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemfmpn  32470  ballotlemsup  32480  ballotlemfrceq  32504  signswch  32549  rpsqrtcn  32582  prodfzo03  32592  itgexpif  32595  bnj1533  32841  bnj1137  32984  bnj1286  33008  bnj1408  33025  bnj1417  33030  subfacp1lem5  33155  cvmsi  33236  gonar  33366  goalr  33368  mpst123  33511  mpstrcl  33512  msrrcl  33514  elmsta  33519  msubvrs  33531  elmpps  33544  elmthm  33547  bcprod  33713  dfon2lem4  33771  oldf  34050  leftirr  34082  rightirr  34083  lrold  34086  sltlpss  34096  pprodss4v  34195  ivthALT  34533  neibastop2lem  34558  nnssi2  34653  nnssi3  34654  bj-sngltagi  35181  bj-elid5  35349  bj-fvmptunsn1  35437  bj-smgrpssmgmel  35449  bj-mndsssmgrpel  35451  bj-cmnssmndel  35453  bj-grpssmndel  35455  bj-ablssgrpel  35457  bj-ablsscmnel  35459  bj-vecssmodel  35462  bj-flddrng  35469  bj-rveccvec  35485  bj-rvecabl  35487  taupilemrplb  35500  icorempo  35531  elxp8  35551  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem14  35800  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  poimirlem32  35818  mblfinlem1  35823  cnambfre  35834  dvtan  35836  itg2addnc  35840  itg2gt0cn  35841  ftc1cnnc  35858  ftc2nc  35868  dvasin  35870  dvacos  35871  cover2  35881  sstotbnd2  35941  heibor1lem  35976  heiborlem10  35987  opidonOLD  36019  exidcl  36043  rngosn3  36091  flddivrng  36166  toycom  36994  osumcllem7N  37983  pexmidlem4N  37994  diaintclN  39079  dibintclN  39188  mapd1o  39669  hdmapevec  39856  dvrelog2  40079  sticksstones1  40109  prjspvs  40456  prjspeclsp  40458  0prjspnrel  40471  elrfi  40523  elrfirn  40524  elrfirn2  40525  mrefg3  40537  diophin  40601  diophun  40602  eq0rabdioph  40605  eqrabdioph  40606  pellex  40664  rmxycomplete  40746  jm2.23  40825  aomclem2  40887  fglmod  40905  lsmfgcl  40906  lmhmfgima  40916  lmhmfgsplit  40918  isnumbasabl  40938  dgrsub2  40967  itgocn  40996  areaquad  41054  nna1iscard  41159  elmapintrab  41191  corcltrcl  41354  k0004val0  41771  elscottab  41869  radcnvrat  41939  uzmptshftfval  41971  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  onfrALTlem2  42173  onfrALTlem2VD  42516  uzwo4  42608  mptssid  42792  uzublem  42977  eliccelioc  43066  elicores  43078  sqrlearg  43098  fsumiunss  43123  limcdm0  43166  sumnnodd  43178  fnlimfvre  43222  limsupubuzlem  43260  limsupmnflem  43268  limsupre3uzlem  43283  climuzlem  43291  cncfshift  43422  cncfperiod  43427  icccncfext  43435  dvnprodlem1  43494  dvnprodlem2  43495  itgsin0pilem1  43498  itgsinexplem1  43502  itgsinexp  43503  ditgeqiooicc  43508  itgsubsticclem  43523  itgioocnicc  43525  itgsbtaddcnst  43530  stoweidlem34  43582  stoweidlem41  43589  stoweidlem51  43599  wallispilem2  43614  stirlinglem11  43632  dirkercncflem2  43652  fourierdlem5  43660  fourierdlem9  43664  fourierdlem17  43672  fourierdlem18  43673  fourierdlem20  43675  fourierdlem39  43694  fourierdlem48  43702  fourierdlem49  43703  fourierdlem62  43716  fourierdlem66  43720  fourierdlem68  43722  fourierdlem72  43726  fourierdlem73  43727  fourierdlem81  43735  fourierdlem83  43737  fourierdlem85  43739  fourierdlem87  43741  fourierdlem88  43742  fourierdlem92  43746  fourierdlem95  43749  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  etransclem24  43806  etransclem35  43817  etransclem37  43819  salexct  43880  salgencntex  43889  sge0resplit  43951  sge0split  43954  meaiuninclem  44025  caratheodorylem1  44071  volicorescl  44098  hoidmv1lelem3  44138  opnvonmbllem2  44178  ovolval2  44189  ovolval3  44192  ovolval4lem1  44194  ovolval4lem2  44195  pimiooltgt  44255  sssmf  44283  smfaddlem1  44308  smflimlem2  44317  smfrec  44334  smfdiv  44342  smfsuplem1  44355  smfsuplem3  44357  fcores  44572  spr0el  44945  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  fldhmsubc  45653  fldhmsubcALTV  45671  fvconst0ci  46197  fvconstdomi  46198  et-ltneverrefl  46521  natglobalincr  46523