Theorem sseli 3943

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 2106   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  sselii  3944  sselid  3945  elun1  4141  elun2  4142  elopabr  5523  elopabran  5524  elopaelxp  5726  copsex2ga  5768  2elresin  6627  nfvres  6888  fvco4i  6947  mptrcl  6962  fvmptss  6965  fvmptex  6967  fvmptnf  6975  elfvmptrab1w  6979  elfvmptrab1  6980  fvopab4ndm  6982  fvimacnvi  7007  elpreima  7013  iinpreima  7024  ofrfvalg  7630  ofval  7633  off  7640  nnon  7813  finds  7840  finds2  7842  eqopi  7962  op1steq  7970  dfoprab4  7992  bropopvvv  8027  bropfvvvv  8029  reldmtpos  8170  wfrlem10OLD  8269  smores2  8305  frsuc  8388  nnfiOLD  9183  unifpw  9306  cantnfp1lem1  9623  cantnfp1lem3  9625  r1fin  9718  r1tr  9721  r1ordg  9723  r1ord3g  9724  r1val1  9731  tz9.12lem3  9734  tcrank  9829  cplem1  9834  hta  9842  tskwe  9895  cardprclem  9924  alephfplem3  10051  dfac12r  10091  ackbij1lem16  10180  ackbij2  10188  fin23lem28  10285  fin23lem30  10287  fin23lem31  10288  fin1a2lem6  10350  hsmexlem4  10374  hsmexlem5  10375  hsmexlem6  10376  axdc2lem  10393  axdc3lem2  10396  axcclem  10402  brdom5  10474  brdom4  10475  r1tskina  10727  gruina  10763  grur1a  10764  pinn  10823  0nnq  10869  elpqn  10870  recn  11150  rexr  11210  ltord1  11690  leord1  11691  eqord1  11692  nnre  12169  nncn  12170  nnind  12180  nnnn0  12429  nn0re  12431  nn0cn  12432  nn0xnn0  12498  nnzOLD  12532  nn0z  12533  nnq  12896  qcn  12897  rpre  12932  eliccxr  13362  difreicc  13411  iccshftri  13414  iccshftli  13416  iccdili  13418  icccntri  13420  fzval2  13437  fzelp1  13503  4fvwrd4  13571  elfzo1  13632  ico01fl0  13734  expcllem  13988  expcl2lem  13989  m1expcl2  14001  bcm1k  14225  bcpasc  14231  hashbclem  14361  wrdv  14429  pfxfv0  14592  pfxfvlsw  14595  cshimadifsn  14730  swrds2m  14842  01sqrexlem5  15143  cau3lem  15251  caubnd  15255  climconst2  15442  o1of2  15507  o1rlimmul  15513  caurcvg  15573  caucvg  15575  binomlem  15725  incexclem  15732  divcnvshft  15751  zprod  15831  fprodge1  15889  risefaccllem  15907  fallfaccllem  15908  bpolydiflem  15948  bpoly4  15953  dvdsflip  16210  divalglem8  16293  sadadd  16358  smumul  16384  isprm3  16570  phimullem  16662  prmdiveq  16669  unbenlem  16791  vdwnnlem1  16878  vdwnnlem3  16880  ramtcl2  16894  prmgaplem4  16937  cshwshashlem1  16979  structcnvcnv  17036  fvsetsid  17051  imasdsval2  17412  mreunirn  17495  mrcfval  17502  mrisval  17524  coapm  17971  tsrss  18492  submnd0  18599  smndex1id  18735  nmzsubg  18981  nmznsg  18984  cntzmhm  19133  symgtrinv  19268  pmtrdifellem4  19275  psgnpmtr  19306  efginvrel2  19523  efginvrel1  19524  efgsp1  19533  efgsres  19534  efgsfo  19535  frgpinv  19560  frgpupf  19569  frgpup1  19571  subcmn  19629  torsubg  19646  dprd2dlem1  19834  dpjidcl  19851  ablfaclem3  19880  nzrring  20205  lringnzr  20221  acsfn1p  20322  lssacs  20485  cnsubdrglem  20885  rege0subm  20890  rge0srg  20905  zringunit  20924  znrrg  21009  psgnghm  21021  zrhpsgnevpm  21032  evpmodpmf1o  21037  pmtrodpm  21038  phlssphl  21100  frlmsslsp  21239  islinds4  21278  lmimlbs  21279  lbslcic  21284  psrbaglefi  21371  psrbaglefiOLD  21372  psrbagconf1o  21375  mplsubglem  21442  mplneg  21451  ressmpladd  21467  ressmplmul  21468  ressmplvsca  21469  mplmonmul  21474  ply1bascl  21611  mdetralt  21994  mdetunilem7  22004  chfacfpmmulgsum2  22251  tgval2  22343  ordtbas  22580  ordtrestixx  22610  hauslly  22880  kgentop  22930  ptbasin  22965  filunirn  23270  uzrest  23285  elflim  23359  flffval  23377  fclsval  23396  isfcls  23397  fcfval  23421  ustn0  23609  fmucndlem  23680  xmetunirn  23727  mopnval  23828  setsmstopn  23870  tmsval  23873  tngtopn  24051  qtopbaslem  24159  xrtgioo  24206  reperflem  24218  icccmplem1  24222  icopnfhmeo  24343  icccvx  24350  bndth  24358  reparphti  24397  pcoval1  24413  pcoval2  24416  pcoass  24424  pcorevlem  24426  pcorev2  24428  pi1xfrcnv  24457  csscld  24650  cfilfval  24665  caufval  24676  bcthlem1  24725  ivthlem1  24852  ivthlem3  24854  ovolicc2lem3  24920  ovolicc2lem4  24921  vitalilem1  25009  mbflimsup  25067  i1fd  25082  i1f0  25088  i1f1  25091  itg1addlem4  25100  itg1addlem4OLD  25101  itg1addlem5  25102  iblmbf  25169  ellimc2  25278  limcres  25287  limcun  25296  dvbsss  25303  perfdvf  25304  dvres2lem  25311  dvaddbr  25339  rolle  25391  cmvth  25392  dvlip  25394  dvlipcn  25395  dvle  25408  lhop1lem  25414  dvfsumle  25422  dvfsumge  25423  dvfsumabs  25424  dvfsumlem2  25428  ftc2  25445  itgparts  25448  itgsubstlem  25449  itgsubst  25450  deg1mul3  25517  coeval  25621  coeeu  25623  dgrval  25626  coef3  25630  coemulc  25653  dgrsub  25670  coecj  25676  dvply2  25683  dvnply  25685  quotval  25689  fta1  25705  plyexmo  25710  aacjcl  25724  taylfval  25755  dvtaylp  25766  abelth  25837  pilem3  25849  cos0pilt1  25925  sinord  25927  recosf1o  25928  resinf1o  25929  tanord1  25930  eff1olem  25941  dvloglem  26040  dvlog  26043  dvlog2lem  26044  advlogexp  26047  logtayl  26052  logtayl2  26054  dvcncxp1  26133  dvcnsqrt  26134  cxpcn3lem  26137  cxpcn3  26138  sqrtcn  26140  loglesqrt  26148  1cubr  26229  acosrecl  26290  efrlim  26356  jensen  26375  lgamgulmlem2  26416  lgamucov2  26425  basellem4  26470  musum  26577  dchrinvcl  26638  dchrghm  26641  dchrinv  26646  dchrsum2  26653  dchrsum  26654  rpvmasumlem  26872  dchrisum0lem2a  26902  pnt  26999  oldf  27230  leftirr  27263  rightirr  27264  lrold  27269  sltlpss  27279  addsproplem2  27325  sleadd1  27341  addsunif  27353  negsproplem2  27370  negsid  27382  negsunif  27393  mulsrid  27420  mulslid  27421  tglng  27551  axlowdimlem6  27959  axlowdimlem16  27969  axlowdimlem17  27970  axlowdim  27973  axeuclidlem  27974  axcontlem2  27977  axcontlem7  27982  axcontlem8  27983  nbusgrvtxm1uvtx  28416  wlk1walk  28650  pthdivtx  28740  pthdadjvtx  28741  crctcshwlkn0lem2  28819  crctcshwlkn0lem4  28821  clwwisshclwws  29022  fusgreg2wsp  29343  nvvcop  29599  nvex  29616  phnv  29819  sheli  30219  cheli  30237  hhssabloilem  30266  choc1  30332  shintcli  30334  chintcli  30336  shsleji  30375  pjini  30704  mayete3i  30733  dmadjop  30893  nlelshi  31065  cnlnadjeui  31082  cnlnssadj  31085  bdopadj  31087  pjimai  31181  stcl  31221  atelch  31349  fcnvgreu  31656  f1od2  31706  fcobijfs  31708  uzssico  31755  iundisj2fi  31768  nnindf  31785  eliccioo  31857  gsummptres  31964  cyc3genpm  32071  elrspunidl  32279  zarcls  32544  ordtrestNEW  32591  xrge0iifcnv  32603  xrge0iifcv  32604  xrge0iifiso  32605  xrge0iifhom  32607  qqhcn  32661  esumval  32734  gsumesum  32747  esumlub  32748  esumcst  32751  esumfsup  32758  issgon  32811  elrnsiga  32814  imambfm  32951  br2base  32958  sxbrsigalem0  32960  dya2iocucvr  32973  sxbrsigalem2  32975  sxbrsigalem5  32977  sxbrsiga  32979  omssubadd  32989  sitmcl  33040  oddpwdc  33043  eulerpartlemelr  33046  eulerpartlemgvv  33065  eulerpartlemgh  33067  eulerpartlemgs2  33069  eulerpartlemn  33070  sseqf  33081  ballotlem2  33177  ballotlemfp1  33180  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemfmpn  33183  ballotlemsup  33193  ballotlemfrceq  33217  signswch  33262  rpsqrtcn  33295  prodfzo03  33305  itgexpif  33308  bnj1533  33553  bnj1137  33696  bnj1286  33720  bnj1408  33737  bnj1417  33742  subfacp1lem5  33865  cvmsi  33946  gonar  34076  goalr  34078  mpst123  34221  mpstrcl  34222  msrrcl  34224  elmsta  34229  msubvrs  34241  elmpps  34254  elmthm  34257  bcprod  34397  dfon2lem4  34447  pprodss4v  34545  ivthALT  34883  neibastop2lem  34908  nnssi2  35003  nnssi3  35004  bj-sngltagi  35526  bj-elid5  35713  bj-fvmptunsn1  35801  bj-smgrpssmgmel  35813  bj-mndsssmgrpel  35815  bj-cmnssmndel  35817  bj-grpssmndel  35819  bj-ablssgrpel  35821  bj-ablsscmnel  35823  bj-vecssmodel  35826  bj-flddrng  35833  bj-rveccvec  35849  bj-rvecabl  35851  taupilemrplb  35864  icorempo  35895  elxp8  35915  sin2h  36141  cos2h  36142  tan2h  36143  poimirlem14  36165  poimirlem26  36177  poimirlem27  36178  poimirlem31  36182  poimirlem32  36183  mblfinlem1  36188  cnambfre  36199  dvtan  36201  itg2addnc  36205  itg2gt0cn  36206  ftc1cnnc  36223  ftc2nc  36233  dvasin  36235  dvacos  36236  cover2  36246  sstotbnd2  36306  heibor1lem  36341  heiborlem10  36352  opidonOLD  36384  exidcl  36408  rngosn3  36456  flddivrng  36531  toycom  37508  osumcllem7N  38498  pexmidlem4N  38509  diaintclN  39594  dibintclN  39703  mapd1o  40184  hdmapevec  40371  dvrelog2  40594  sticksstones1  40627  imacrhmcl  40762  prjspvs  41006  prjspeclsp  41008  0prjspnrel  41023  elrfi  41075  elrfirn  41076  elrfirn2  41077  mrefg3  41089  diophin  41153  diophun  41154  eq0rabdioph  41157  eqrabdioph  41158  pellex  41216  rmxycomplete  41299  jm2.23  41378  aomclem2  41440  fglmod  41458  lsmfgcl  41459  lmhmfgima  41469  lmhmfgsplit  41471  isnumbasabl  41491  dgrsub2  41520  itgocn  41549  areaquad  41608  cantnftermord  41713  omabs2  41725  nna1iscard  41939  elmapintrab  41970  corcltrcl  42133  k0004val0  42548  elscottab  42646  radcnvrat  42716  uzmptshftfval  42748  binomcxplemdvsum  42757  binomcxplemnotnn0  42758  onfrALTlem2  42950  onfrALTlem2VD  43293  uzwo4  43383  mptssid  43588  uzublem  43785  eliccelioc  43879  elicores  43891  sqrlearg  43911  fsumiunss  43936  limcdm0  43979  sumnnodd  43991  fnlimfvre  44035  limsupubuzlem  44073  limsupmnflem  44081  limsupre3uzlem  44096  climuzlem  44104  cncfshift  44235  cncfperiod  44240  icccncfext  44248  dvnprodlem1  44307  dvnprodlem2  44308  itgsin0pilem1  44311  itgsinexplem1  44315  itgsinexp  44316  ditgeqiooicc  44321  itgsubsticclem  44336  itgioocnicc  44338  itgsbtaddcnst  44343  stoweidlem34  44395  stoweidlem41  44402  stoweidlem51  44412  wallispilem2  44427  stirlinglem11  44445  dirkercncflem2  44465  fourierdlem5  44473  fourierdlem9  44477  fourierdlem17  44485  fourierdlem18  44486  fourierdlem20  44488  fourierdlem39  44507  fourierdlem48  44515  fourierdlem49  44516  fourierdlem62  44529  fourierdlem66  44533  fourierdlem68  44535  fourierdlem72  44539  fourierdlem73  44540  fourierdlem81  44548  fourierdlem83  44550  fourierdlem85  44552  fourierdlem87  44554  fourierdlem88  44555  fourierdlem92  44559  fourierdlem95  44562  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  sqwvfoura  44589  sqwvfourb  44590  fouriersw  44592  etransclem24  44619  etransclem35  44630  etransclem37  44632  salexct  44695  salgencntex  44704  sge0resplit  44767  sge0split  44770  meaiuninclem  44841  caratheodorylem1  44887  volicorescl  44914  hoidmv1lelem3  44954  opnvonmbllem2  44994  ovolval2  45005  ovolval3  45008  ovolval4lem1  45010  ovolval4lem2  45011  pimiooltgt  45071  sssmf  45099  smfaddlem1  45124  smflimlem2  45133  smfrec  45150  smfdiv  45158  smfsuplem1  45172  smfsuplem3  45174  et-ltneverrefl  45232  natglobalincr  45236  fcores  45421  spr0el  45794  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbnd  46121  fldhmsubc  46502  fldhmsubcALTV  46520  fvconst0ci  47045  fvconstdomi  47046