Theorem sseli 3928

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3900

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 2112

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

This theorem is referenced by:  sselii  3929  sselid  3930  elun1  4130  elun2  4131  elopabr  5498  elopabran  5499  elopaelxp  5704  copsex2ga  5745  2elresin  6598  nfvres  6855  fvco4i  6918  mptrcl  6933  fvmptss  6936  fvmptex  6938  fvmptnf  6946  elfvmptrab1w  6951  elfvmptrab1  6952  fvopab4ndm  6954  fvimacnvi  6980  elpreima  6986  iinpreima  6997  ofrfvalg  7613  ofval  7616  off  7623  nnon  7797  finds  7821  finds2  7823  eqopi  7952  op1steq  7960  dfoprab4  7982  bropopvvv  8015  bropfvvvv  8017  reldmtpos  8159  smores2  8269  frsuc  8351  unifpw  9234  cantnfp1lem1  9563  cantnfp1lem3  9565  r1fin  9658  r1tr  9661  r1ordg  9663  r1ord3g  9664  r1val1  9671  tz9.12lem3  9674  tcrank  9769  cplem1  9774  hta  9782  tskwe  9835  cardprclem  9864  alephfplem3  9989  dfac12r  10030  ackbij1lem16  10117  ackbij2  10125  fin23lem28  10223  fin23lem30  10225  fin23lem31  10226  fin1a2lem6  10288  hsmexlem4  10312  hsmexlem5  10313  hsmexlem6  10314  axdc2lem  10331  axdc3lem2  10334  axcclem  10340  brdom5  10412  brdom4  10413  r1tskina  10665  gruina  10701  grur1a  10702  pinn  10761  0nnq  10807  elpqn  10808  recn  11088  rexr  11150  ltord1  11635  leord1  11636  eqord1  11637  nnre  12124  nncn  12125  nnind  12135  nnnn0  12380  nn0re  12382  nn0cn  12383  nn0xnn0  12450  nnzOLD  12484  nn0z  12485  uzuzle35  12777  nnq  12852  qcn  12853  rpre  12891  eliccxr  13327  difreicc  13376  iccshftri  13379  iccshftli  13381  iccdili  13383  icccntri  13385  fzval2  13402  fzelp1  13468  4fvwrd4  13540  elfzo1  13604  ico01fl0  13715  expcllem  13971  expcl2lem  13972  m1expcl2  13984  bcm1k  14214  bcpasc  14220  hashbclem  14351  wrdv  14428  pfxfv0  14591  pfxfvlsw  14594  cshimadifsn  14728  swrds2m  14840  01sqrexlem5  15145  cau3lem  15254  caubnd  15258  climconst2  15447  o1of2  15512  o1rlimmul  15518  caurcvg  15576  caucvg  15578  binomlem  15728  incexclem  15735  divcnvshft  15754  zprod  15836  fprodge1  15894  risefaccllem  15912  fallfaccllem  15913  bpolydiflem  15953  bpoly4  15958  dvdsflip  16220  divalglem8  16303  sadadd  16370  smumul  16396  isprm3  16586  phimullem  16682  prmdiveq  16689  unbenlem  16812  vdwnnlem1  16899  vdwnnlem3  16901  ramtcl2  16915  prmgaplem4  16958  cshwshashlem1  16999  structcnvcnv  17056  fvsetsid  17071  imasdsval2  17412  mreunirn  17495  mrcfval  17506  mrisval  17528  coapm  17970  tsrss  18487  chnccat  18524  ex-chn1  18535  submnd0  18663  smndex1id  18811  nmzsubg  19070  nmznsg  19073  cntzmhm  19246  symgtrinv  19377  pmtrdifellem4  19384  psgnpmtr  19415  efginvrel2  19632  efginvrel1  19633  efgsp1  19642  efgsres  19643  efgsfo  19644  frgpinv  19669  frgpupf  19678  frgpup1  19680  subcmn  19742  torsubg  19759  dprd2dlem1  19948  dpjidcl  19965  ablfaclem3  19994  nzrring  20424  lringnzr  20449  fldhmsubc  20693  acsfn1p  20707  lssacs  20893  cnsubdrglem  21348  rege0subm  21353  rge0srg  21368  zringunit  21396  znrrg  21495  psgnghm  21510  zrhpsgnevpm  21521  evpmodpmf1o  21526  pmtrodpm  21527  phlssphl  21589  frlmsslsp  21726  islinds4  21765  lmimlbs  21766  lbslcic  21771  psrbaglefi  21856  psrbagconf1o  21859  mplsubglem  21929  mplneg  21940  ressmpladd  21957  ressmplmul  21958  ressmplvsca  21959  mplmonmul  21964  psdmul  22074  ply1bascl  22109  mdetralt  22516  mdetunilem7  22526  chfacfpmmulgsum2  22773  tgval2  22864  ordtbas  23100  ordtrestixx  23130  hauslly  23400  kgentop  23450  ptbasin  23485  filunirn  23790  uzrest  23805  elflim  23879  flffval  23897  fclsval  23916  isfcls  23917  fcfval  23941  ustn0  24129  fmucndlem  24198  xmetunirn  24245  mopnval  24346  setsmstopn  24386  tmsval  24389  tngtopn  24558  qtopbaslem  24666  xrtgioo  24715  reperflem  24727  icccmplem1  24731  icopnfhmeo  24861  icccvx  24868  bndth  24877  reparphtiOLD  24917  pcoval1  24933  pcoval2  24936  pcoass  24944  pcorevlem  24946  pcorev2  24948  pi1xfrcnv  24977  csscld  25169  cfilfval  25184  caufval  25195  bcthlem1  25244  ivthlem1  25372  ivthlem3  25374  ovolicc2lem3  25440  ovolicc2lem4  25441  vitalilem1  25529  mbflimsup  25587  i1fd  25602  i1f0  25608  i1f1  25611  itg1addlem4  25620  itg1addlem5  25621  iblmbf  25688  ellimc2  25798  limcres  25807  limcun  25816  dvbsss  25823  perfdvf  25824  dvres2lem  25831  dvaddbr  25860  rolle  25914  cmvth  25915  cmvthOLD  25916  dvlip  25918  dvlipcn  25919  dvle  25932  lhop1lem  25938  dvfsumle  25946  dvfsumleOLD  25947  dvfsumge  25948  dvfsumabs  25949  dvfsumlem2  25953  dvfsumlem2OLD  25954  ftc2  25971  itgparts  25974  itgsubstlem  25975  itgsubst  25976  deg1mul3  26041  coeval  26148  coeeu  26150  dgrval  26153  coef3  26157  coemulc  26180  dgrsub  26198  coecj  26204  coecjOLD  26206  dvply2  26214  dvnply  26216  quotval  26220  fta1  26236  plyexmo  26241  aacjcl  26255  taylfval  26286  dvtaylp  26298  abelth  26371  pilem3  26383  cos0pilt1  26461  sinord  26463  recosf1o  26464  resinf1o  26465  tanord1  26466  eff1olem  26477  dvloglem  26577  dvlog  26580  dvlog2lem  26581  advlogexp  26584  logtayl  26589  logtayl2  26591  dvcncxp1  26672  dvcnsqrt  26673  cxpcn3lem  26677  cxpcn3  26678  sqrtcn  26680  loglesqrt  26691  1cubr  26772  acosrecl  26833  efrlim  26899  efrlimOLD  26900  jensen  26919  lgamgulmlem2  26960  lgamucov2  26969  basellem4  27014  musum  27121  mpodvdsmulf1o  27124  fsumdvdsmul  27125  dchrinvcl  27184  dchrghm  27187  dchrinv  27192  dchrsum2  27199  dchrsum  27200  rpvmasumlem  27418  dchrisum0lem2a  27448  pnt  27545  oldf  27791  leftirr  27829  rightirr  27830  lrold  27835  newbdayim  27841  sltlpss  27846  addsproplem2  27906  sleadd1  27925  addsuniflem  27937  addsbdaylem  27952  addsbday  27953  negsproplem2  27964  negsid  27976  negsunif  27990  mulsrid  28045  mulsproplem12  28059  mulsproplem13  28060  mulsproplem14  28061  precsexlem9  28146  precsexlem11  28148  onsno  28185  onscutlt  28194  onaddscl  28203  onmulscl  28204  n0sno  28245  nnsno  28246  nnn0s  28249  nnsgt0  28260  zno  28299  expscllem  28346  tglng  28517  axlowdimlem6  28918  axlowdimlem16  28928  axlowdimlem17  28929  axlowdim  28932  axeuclidlem  28933  axcontlem2  28936  axcontlem7  28941  axcontlem8  28942  nbusgrvtxm1uvtx  29376  wlk1walk  29610  pthdivtx  29698  pthdadjvtx  29699  crctcshwlkn0lem2  29782  crctcshwlkn0lem4  29784  clwwisshclwws  29985  fusgreg2wsp  30306  nvvcop  30564  nvex  30581  phnv  30784  sheli  31184  cheli  31202  hhssabloilem  31231  choc1  31297  shintcli  31299  chintcli  31301  shsleji  31340  pjini  31669  mayete3i  31698  dmadjop  31858  nlelshi  32030  cnlnadjeui  32047  cnlnssadj  32050  bdopadj  32052  pjimai  32146  stcl  32186  atelch  32314  fcnvgreu  32645  f1od2  32692  fcobijfs  32694  fcobijfs2  32695  uzssico  32757  iundisj2fi  32769  nnindf  32792  eliccioo  32901  gsummptres  33022  cyc3genpm  33111  elrspunidl  33383  zarcls  33877  ordtrestNEW  33924  xrge0iifcnv  33936  xrge0iifcv  33937  xrge0iifiso  33938  xrge0iifhom  33940  qqhcn  33994  esumval  34049  gsumesum  34062  esumlub  34063  esumcst  34066  esumfsup  34073  issgon  34126  elrnsiga  34129  imambfm  34265  br2base  34272  sxbrsigalem0  34274  dya2iocucvr  34287  sxbrsigalem2  34289  sxbrsigalem5  34291  sxbrsiga  34293  omssubadd  34303  sitmcl  34354  oddpwdc  34357  eulerpartlemelr  34360  eulerpartlemgvv  34379  eulerpartlemgh  34381  eulerpartlemgs2  34383  eulerpartlemn  34384  sseqf  34395  ballotlem2  34492  ballotlemfp1  34495  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemfmpn  34498  ballotlemsup  34508  ballotlemfrceq  34532  signswch  34564  rpsqrtcn  34596  prodfzo03  34606  itgexpif  34609  bnj1533  34854  bnj1137  34997  bnj1286  35021  bnj1408  35038  bnj1417  35043  onvf1odlem4  35118  subfacp1lem5  35196  cvmsi  35277  gonar  35407  goalr  35409  mpst123  35552  mpstrcl  35553  msrrcl  35555  elmsta  35560  msubvrs  35572  elmpps  35585  elmthm  35588  bcprod  35750  dfon2lem4  35799  pprodss4v  35897  ivthALT  36348  neibastop2lem  36373  nnssi2  36468  nnssi3  36469  bj-sngltagi  36995  bj-elid5  37182  bj-fvmptunsn1  37270  bj-smgrpssmgmel  37282  bj-mndsssmgrpel  37284  bj-cmnssmndel  37286  bj-grpssmndel  37288  bj-ablssgrpel  37290  bj-ablsscmnel  37292  bj-vecssmodel  37295  bj-flddrng  37302  bj-rveccvec  37318  bj-rvecabl  37320  taupilemrplb  37333  icorempo  37364  elxp8  37384  sin2h  37629  cos2h  37630  tan2h  37631  poimirlem14  37653  poimirlem26  37665  poimirlem27  37666  poimirlem31  37670  poimirlem32  37671  mblfinlem1  37676  cnambfre  37687  dvtan  37689  itg2addnc  37693  itg2gt0cn  37694  ftc1cnnc  37711  ftc2nc  37721  dvasin  37723  dvacos  37724  cover2  37734  sstotbnd2  37793  heibor1lem  37828  heiborlem10  37839  opidonOLD  37871  exidcl  37895  rngosn3  37943  flddivrng  38018  toycom  38991  osumcllem7N  39980  pexmidlem4N  39991  diaintclN  41076  dibintclN  41185  mapd1o  41666  hdmapevec  41853  dvrelog2  42076  aks6d1c2lem4  42139  sticksstones1  42158  aks6d1c6lem5  42189  redvmptabs  42372  imacrhmcl  42526  prjspvs  42622  prjspeclsp  42624  0prjspnrel  42639  elrfi  42706  elrfirn  42707  elrfirn2  42708  mrefg3  42720  diophin  42784  diophun  42785  eq0rabdioph  42788  eqrabdioph  42789  pellex  42847  rmxycomplete  42929  jm2.23  43008  aomclem2  43067  fglmod  43085  lsmfgcl  43086  lmhmfgima  43096  lmhmfgsplit  43098  isnumbasabl  43118  dgrsub2  43147  itgocn  43176  areaquad  43228  cantnftermord  43332  omabs2  43344  nna1iscard  43557  elmapintrab  43588  corcltrcl  43751  k0004val0  44166  elscottab  44256  radcnvrat  44326  uzmptshftfval  44358  binomcxplemdvsum  44367  binomcxplemnotnn0  44368  onfrALTlem2  44558  onfrALTlem2VD  44900  uzwo4  45069  mptssid  45257  uzublem  45447  eliccelioc  45540  elicores  45552  sqrlearg  45572  fsumiunss  45594  limcdm0  45637  sumnnodd  45649  fnlimfvre  45691  limsupubuzlem  45729  limsupmnflem  45737  limsupre3uzlem  45752  climuzlem  45760  liminflelimsuplem  45792  cncfshift  45891  cncfperiod  45896  icccncfext  45904  dvnprodlem1  45963  dvnprodlem2  45964  itgsin0pilem1  45967  itgsinexplem1  45971  itgsinexp  45972  ditgeqiooicc  45977  itgsubsticclem  45992  itgioocnicc  45994  itgsbtaddcnst  45999  stoweidlem34  46051  stoweidlem41  46058  stoweidlem51  46068  wallispilem2  46083  stirlinglem11  46101  dirkercncflem2  46121  fourierdlem5  46129  fourierdlem9  46133  fourierdlem17  46141  fourierdlem18  46142  fourierdlem20  46144  fourierdlem39  46163  fourierdlem48  46171  fourierdlem49  46172  fourierdlem62  46185  fourierdlem66  46189  fourierdlem68  46191  fourierdlem72  46195  fourierdlem73  46196  fourierdlem81  46204  fourierdlem83  46206  fourierdlem85  46208  fourierdlem87  46210  fourierdlem88  46211  fourierdlem92  46215  fourierdlem95  46218  fourierdlem103  46226  fourierdlem104  46227  fourierdlem112  46235  sqwvfoura  46245  sqwvfourb  46246  fouriersw  46248  etransclem24  46275  etransclem35  46286  etransclem37  46288  salexct  46351  salgencntex  46360  sge0resplit  46423  sge0split  46426  meaiuninclem  46497  caratheodorylem1  46543  volicorescl  46570  hoidmv1lelem3  46610  opnvonmbllem2  46650  ovolval2  46661  ovolval3  46664  ovolval4lem1  46666  ovolval4lem2  46667  pimiooltgt  46727  sssmf  46755  smfaddlem1  46780  smflimlem2  46789  smfrec  46806  smfdiv  46814  smfsuplem1  46828  smfsuplem3  46830  et-ltneverrefl  46888  natglobalincr  46894  tannpoly  46900  fcores  47077  rehalfge1  47345  spr0el  47492  bgoldbtbndlem2  47816  bgoldbtbndlem3  47817  bgoldbtbnd  47819  upgrimpthslem2  47918  stgredgiun  47968  isubgr3stgrlem7  47982  fldhmsubcALTV  48343  fvconst0ci  48901  fvconstdomi  48902  idfullsubc  49172  fulloppf  49174  fthoppf  49175  initopropdlemlem  49250