Theorem sseli 3917

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 2114   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906

This theorem is referenced by:  sselii  3918  sselid  3919  elun1  4122  elun2  4123  elopabr  5515  elopabran  5516  elopaelxp  5721  copsex2ga  5763  2elresin  6619  nfvres  6878  fvco4i  6941  mptrcl  6957  fvmptss  6960  fvmptex  6962  fvmptnf  6970  elfvmptrab1w  6975  elfvmptrab1  6976  fvopab4ndm  6978  fvimacnvi  7004  elpreima  7010  iinpreima  7021  ofrfvalg  7639  ofval  7642  off  7649  nnon  7823  finds  7847  finds2  7849  eqopi  7978  op1steq  7986  dfoprab4  8008  bropopvvv  8040  bropfvvvv  8042  reldmtpos  8184  smores2  8294  frsuc  8376  unifpw  9265  cantnfp1lem1  9599  cantnfp1lem3  9601  r1fin  9697  r1tr  9700  r1ordg  9702  r1ord3g  9703  r1val1  9710  tz9.12lem3  9713  tcrank  9808  cplem1  9813  hta  9821  tskwe  9874  cardprclem  9903  alephfplem3  10028  dfac12r  10069  ackbij1lem16  10156  ackbij2  10164  fin23lem28  10262  fin23lem30  10264  fin23lem31  10265  fin1a2lem6  10327  hsmexlem4  10351  hsmexlem5  10352  hsmexlem6  10353  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  brdom5  10451  brdom4  10452  r1tskina  10705  gruina  10741  grur1a  10742  pinn  10801  0nnq  10847  elpqn  10848  recn  11128  rexr  11191  ltord1  11676  leord1  11677  eqord1  11678  nnre  12181  nncn  12182  nnind  12192  nnnn0  12444  nn0re  12446  nn0cn  12447  nn0xnn0  12514  nn0z  12548  uzuzle35  12837  nnq  12912  qcn  12913  rpre  12951  eliccxr  13388  difreicc  13437  iccshftri  13440  iccshftli  13442  iccdili  13444  icccntri  13446  fzval2  13464  fzelp1  13530  4fvwrd4  13602  elfzo1  13667  ico01fl0  13778  expcllem  14034  expcl2lem  14035  m1expcl2  14047  bcm1k  14277  bcpasc  14283  hashbclem  14414  wrdv  14491  pfxfv0  14654  pfxfvlsw  14657  cshimadifsn  14791  swrds2m  14903  01sqrexlem5  15208  cau3lem  15317  caubnd  15321  climconst2  15510  o1of2  15575  o1rlimmul  15581  caurcvg  15639  caucvg  15641  binomlem  15794  incexclem  15801  divcnvshft  15820  zprod  15902  fprodge1  15960  risefaccllem  15978  fallfaccllem  15979  bpolydiflem  16019  bpoly4  16024  dvdsflip  16286  divalglem8  16369  sadadd  16436  smumul  16462  isprm3  16652  phimullem  16749  prmdiveq  16756  unbenlem  16879  vdwnnlem1  16966  vdwnnlem3  16968  ramtcl2  16982  prmgaplem4  17025  cshwshashlem1  17066  structcnvcnv  17123  fvsetsid  17138  imasdsval2  17480  mreunirn  17563  mrcfval  17574  mrisval  17596  coapm  18038  tsrss  18555  chnccat  18592  ex-chn1  18603  submnd0  18731  smndex1id  18882  nmzsubg  19140  nmznsg  19143  cntzmhm  19316  symgtrinv  19447  pmtrdifellem4  19454  psgnpmtr  19485  efginvrel2  19702  efginvrel1  19703  efgsp1  19712  efgsres  19713  efgsfo  19714  frgpinv  19739  frgpupf  19748  frgpup1  19750  subcmn  19812  torsubg  19829  dprd2dlem1  20018  dpjidcl  20035  ablfaclem3  20064  nzrring  20493  lringnzr  20518  fldhmsubc  20762  acsfn1p  20776  lssacs  20962  cnsubdrglem  21398  rege0subm  21403  rge0srg  21418  zringunit  21446  znrrg  21545  psgnghm  21560  zrhpsgnevpm  21571  evpmodpmf1o  21576  pmtrodpm  21577  phlssphl  21639  frlmsslsp  21776  islinds4  21815  lmimlbs  21816  lbslcic  21821  psrbaglefi  21906  psrbagconf1o  21909  mplsubglem  21977  mplneg  21988  ressmpladd  22007  ressmplmul  22008  ressmplvsca  22009  mplmonmul  22014  psdmul  22132  ply1bascl  22167  mdetralt  22573  mdetunilem7  22583  chfacfpmmulgsum2  22830  tgval2  22921  ordtbas  23157  ordtrestixx  23187  hauslly  23457  kgentop  23507  ptbasin  23542  filunirn  23847  uzrest  23862  elflim  23936  flffval  23954  fclsval  23973  isfcls  23974  fcfval  23998  ustn0  24186  fmucndlem  24255  xmetunirn  24302  mopnval  24403  setsmstopn  24443  tmsval  24446  tngtopn  24615  qtopbaslem  24723  xrtgioo  24772  reperflem  24784  icccmplem1  24788  icopnfhmeo  24910  icccvx  24917  bndth  24925  pcoval1  24980  pcoval2  24983  pcoass  24991  pcorevlem  24993  pcorev2  24995  pi1xfrcnv  25024  csscld  25216  cfilfval  25231  caufval  25242  bcthlem1  25291  ivthlem1  25418  ivthlem3  25420  ovolicc2lem3  25486  ovolicc2lem4  25487  vitalilem1  25575  mbflimsup  25633  i1fd  25648  i1f0  25654  i1f1  25657  itg1addlem4  25666  itg1addlem5  25667  iblmbf  25734  ellimc2  25844  limcres  25853  limcun  25862  dvbsss  25869  perfdvf  25870  dvres2lem  25877  dvaddbr  25905  rolle  25957  cmvth  25958  dvlip  25960  dvlipcn  25961  dvle  25974  lhop1lem  25980  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem2  25994  ftc2  26011  itgparts  26014  itgsubstlem  26015  itgsubst  26016  deg1mul3  26081  coeval  26188  coeeu  26190  dgrval  26193  coef3  26197  coemulc  26220  dgrsub  26237  coecj  26243  coecjOLD  26245  dvply2  26252  dvnply  26254  quotval  26258  fta1  26274  plyexmo  26279  aacjcl  26293  taylfval  26324  dvtaylp  26335  abelth  26406  pilem3  26418  cos0pilt1  26496  sinord  26498  recosf1o  26499  resinf1o  26500  tanord1  26501  eff1olem  26512  dvloglem  26612  dvlog  26615  dvlog2lem  26616  advlogexp  26619  logtayl  26624  logtayl2  26626  dvcncxp1  26707  dvcnsqrt  26708  cxpcn3lem  26711  cxpcn3  26712  sqrtcn  26714  loglesqrt  26725  1cubr  26806  acosrecl  26867  efrlim  26933  jensen  26952  lgamgulmlem2  26993  lgamucov2  27002  basellem4  27047  musum  27154  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dchrinvcl  27216  dchrghm  27219  dchrinv  27224  dchrsum2  27231  dchrsum  27232  rpvmasumlem  27450  dchrisum0lem2a  27480  pnt  27577  oldf  27829  madeno  27835  oldno  27836  newno  27837  oldmade  27860  leftold  27867  rightold  27868  leftno  27869  rightno  27870  addbdaylem  28009  addbday  28010  negsproplem2  28021  negsid  28033  negsunif  28047  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  precsexlem11  28209  onno  28247  oncutlt  28256  n0no  28315  nnno  28316  nnn0s  28319  nnsgt0  28331  zno  28374  expscllem  28422  tglng  28614  axlowdimlem6  29016  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  axeuclidlem  29031  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  nbusgrvtxm1uvtx  29474  wlk1walk  29707  pthdivtx  29795  pthdadjvtx  29796  crctcshwlkn0lem2  29879  crctcshwlkn0lem4  29881  clwwisshclwws  30085  fusgreg2wsp  30406  nvvcop  30665  nvex  30682  phnv  30885  sheli  31285  cheli  31303  hhssabloilem  31332  choc1  31398  shintcli  31400  chintcli  31402  shsleji  31441  pjini  31770  mayete3i  31799  dmadjop  31959  nlelshi  32131  cnlnadjeui  32148  cnlnssadj  32151  bdopadj  32153  pjimai  32247  stcl  32287  atelch  32415  fcnvgreu  32745  f1od2  32792  fcobijfs  32794  fcobijfs2  32795  uzssico  32857  iundisj2fi  32870  nnindf  32893  eliccioo  32990  gsummptres  33113  cyc3genpm  33213  elrspunidl  33488  psrmonmul  33694  zarcls  34018  ordtrestNEW  34065  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  qqhcn  34135  esumval  34190  gsumesum  34203  esumlub  34204  esumcst  34207  esumfsup  34214  issgon  34267  elrnsiga  34270  imambfm  34406  br2base  34413  sxbrsigalem0  34415  dya2iocucvr  34428  sxbrsigalem2  34430  sxbrsigalem5  34432  sxbrsiga  34434  omssubadd  34444  sitmcl  34495  oddpwdc  34498  eulerpartlemelr  34501  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemgs2  34524  eulerpartlemn  34525  sseqf  34536  ballotlem2  34633  ballotlemfp1  34636  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemfmpn  34639  ballotlemsup  34649  ballotlemfrceq  34673  signswch  34705  rpsqrtcn  34737  prodfzo03  34747  itgexpif  34750  bnj1533  34994  bnj1137  35137  bnj1286  35161  bnj1408  35178  bnj1417  35183  r1omhf  35249  onvf1odlem4  35288  subfacp1lem5  35366  cvmsi  35447  gonar  35577  goalr  35579  mpst123  35722  mpstrcl  35723  msrrcl  35725  elmsta  35730  msubvrs  35742  elmpps  35755  elmthm  35758  bcprod  35920  dfon2lem4  35966  pprodss4v  36064  ivthALT  36517  neibastop2lem  36542  nnssi2  36637  nnssi3  36638  ttcel2  36683  bj-sngltagi  37289  bj-elid5  37483  bj-fvmptunsn1  37571  bj-smgrpssmgmel  37583  bj-mndsssmgrpel  37585  bj-cmnssmndel  37587  bj-grpssmndel  37589  bj-ablssgrpel  37591  bj-ablsscmnel  37593  bj-vecssmodel  37596  bj-flddrng  37603  bj-rveccvec  37619  bj-rvecabl  37621  taupilemrplb  37634  icorempo  37667  elxp8  37687  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem14  37955  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  mblfinlem1  37978  cnambfre  37989  dvtan  37991  itg2addnc  37995  itg2gt0cn  37996  ftc1cnnc  38013  ftc2nc  38023  dvasin  38025  dvacos  38026  cover2  38036  sstotbnd2  38095  heibor1lem  38130  heiborlem10  38141  opidonOLD  38173  exidcl  38197  rngosn3  38245  flddivrng  38320  toycom  39419  osumcllem7N  40408  pexmidlem4N  40419  diaintclN  41504  dibintclN  41613  mapd1o  42094  hdmapevec  42281  dvrelog2  42503  aks6d1c2lem4  42566  sticksstones1  42585  aks6d1c6lem5  42616  redvmptabs  42792  imacrhmcl  42959  prjspvs  43043  prjspeclsp  43045  0prjspnrel  43060  elrfi  43126  elrfirn  43127  elrfirn2  43128  mrefg3  43140  diophin  43204  diophun  43205  eq0rabdioph  43208  eqrabdioph  43209  pellex  43263  rmxycomplete  43345  jm2.23  43424  aomclem2  43483  fglmod  43501  lsmfgcl  43502  lmhmfgima  43512  lmhmfgsplit  43514  isnumbasabl  43534  dgrsub2  43563  itgocn  43592  areaquad  43644  cantnftermord  43748  omabs2  43760  nna1iscard  43972  elmapintrab  44003  corcltrcl  44166  k0004val0  44581  elscottab  44671  radcnvrat  44741  uzmptshftfval  44773  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  onfrALTlem2  44973  onfrALTlem2VD  45315  uzwo4  45484  mptssid  45670  uzublem  45858  eliccelioc  45951  elicores  45963  sqrlearg  45983  fsumiunss  46005  limcdm0  46048  sumnnodd  46060  fnlimfvre  46102  limsupubuzlem  46140  limsupmnflem  46148  limsupre3uzlem  46163  climuzlem  46171  liminflelimsuplem  46203  cncfshift  46302  cncfperiod  46307  icccncfext  46315  dvnprodlem1  46374  dvnprodlem2  46375  itgsin0pilem1  46378  itgsinexplem1  46382  itgsinexp  46383  ditgeqiooicc  46388  itgsubsticclem  46403  itgioocnicc  46405  itgsbtaddcnst  46410  stoweidlem34  46462  stoweidlem41  46469  stoweidlem51  46479  wallispilem2  46494  stirlinglem11  46512  dirkercncflem2  46532  fourierdlem5  46540  fourierdlem9  46544  fourierdlem17  46552  fourierdlem18  46553  fourierdlem20  46555  fourierdlem39  46574  fourierdlem48  46582  fourierdlem49  46583  fourierdlem62  46596  fourierdlem66  46600  fourierdlem68  46602  fourierdlem72  46606  fourierdlem73  46607  fourierdlem81  46615  fourierdlem83  46617  fourierdlem85  46619  fourierdlem87  46621  fourierdlem88  46622  fourierdlem92  46626  fourierdlem95  46629  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  etransclem24  46686  etransclem35  46697  etransclem37  46699  salexct  46762  salgencntex  46771  sge0resplit  46834  sge0split  46837  meaiuninclem  46908  caratheodorylem1  46954  volicorescl  46981  hoidmv1lelem3  47021  opnvonmbllem2  47061  ovolval2  47072  ovolval3  47075  ovolval4lem1  47077  ovolval4lem2  47078  sssmf  47166  smfaddlem1  47191  smflimlem2  47200  smfrec  47217  smfdiv  47225  smfsuplem1  47239  smfsuplem3  47241  et-ltneverrefl  47299  natglobalincr  47307  tannpoly  47338  fcores  47515  elfz2nn  47770  rehalfge1  47787  spr0el  47942  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  ppivalnnnprmge6  48089  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  upgrimpthslem2  48384  stgredgiun  48434  isubgr3stgrlem7  48448  fldhmsubcALTV  48809  fvconst0ci  49366  fvconstdomi  49367  idfullsubc  49636  fulloppf  49638  fthoppf  49639  initopropdlemlem  49714