Theorem sseli 3974

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

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-clel 2803  df-ss 3963

This theorem is referenced by:  sselii  3975  sselid  3976  elun1  4174  elun2  4175  elopabr  5559  elopabran  5560  elopaelxp  5763  copsex2ga  5805  2elresin  6674  nfvres  6934  fvco4i  6995  mptrcl  7010  fvmptss  7013  fvmptex  7015  fvmptnf  7023  elfvmptrab1w  7028  elfvmptrab1  7029  fvopab4ndm  7031  fvimacnvi  7057  elpreima  7063  iinpreima  7074  ofrfvalg  7690  ofval  7693  off  7700  nnon  7874  finds  7901  finds2  7903  eqopi  8031  op1steq  8039  dfoprab4  8061  bropopvvv  8096  bropfvvvv  8098  reldmtpos  8241  wfrlem10OLD  8340  smores2  8376  frsuc  8459  nnfiOLD  9259  unifpw  9392  cantnfp1lem1  9714  cantnfp1lem3  9716  r1fin  9809  r1tr  9812  r1ordg  9814  r1ord3g  9815  r1val1  9822  tz9.12lem3  9825  tcrank  9920  cplem1  9925  hta  9933  tskwe  9986  cardprclem  10015  alephfplem3  10142  dfac12r  10182  ackbij1lem16  10269  ackbij2  10277  fin23lem28  10374  fin23lem30  10376  fin23lem31  10377  fin1a2lem6  10439  hsmexlem4  10463  hsmexlem5  10464  hsmexlem6  10465  axdc2lem  10482  axdc3lem2  10485  axcclem  10491  brdom5  10563  brdom4  10564  r1tskina  10816  gruina  10852  grur1a  10853  pinn  10912  0nnq  10958  elpqn  10959  recn  11239  rexr  11301  ltord1  11781  leord1  11782  eqord1  11783  nnre  12265  nncn  12266  nnind  12276  nnnn0  12525  nn0re  12527  nn0cn  12528  nn0xnn0  12594  nnzOLD  12628  nn0z  12629  nnq  12992  qcn  12993  rpre  13030  eliccxr  13460  difreicc  13509  iccshftri  13512  iccshftli  13514  iccdili  13516  icccntri  13518  fzval2  13535  fzelp1  13601  4fvwrd4  13669  elfzo1  13730  ico01fl0  13833  expcllem  14086  expcl2lem  14087  m1expcl2  14099  bcm1k  14327  bcpasc  14333  hashbclem  14464  wrdv  14532  pfxfv0  14695  pfxfvlsw  14698  cshimadifsn  14833  swrds2m  14945  01sqrexlem5  15246  cau3lem  15354  caubnd  15358  climconst2  15545  o1of2  15610  o1rlimmul  15616  caurcvg  15676  caucvg  15678  binomlem  15828  incexclem  15835  divcnvshft  15854  zprod  15934  fprodge1  15992  risefaccllem  16010  fallfaccllem  16011  bpolydiflem  16051  bpoly4  16056  dvdsflip  16314  divalglem8  16397  sadadd  16462  smumul  16488  isprm3  16679  phimullem  16776  prmdiveq  16783  unbenlem  16905  vdwnnlem1  16992  vdwnnlem3  16994  ramtcl2  17008  prmgaplem4  17051  cshwshashlem1  17093  structcnvcnv  17150  fvsetsid  17165  imasdsval2  17526  mreunirn  17609  mrcfval  17616  mrisval  17638  coapm  18088  tsrss  18609  submnd0  18751  smndex1id  18896  nmzsubg  19155  nmznsg  19158  cntzmhm  19331  symgtrinv  19466  pmtrdifellem4  19473  psgnpmtr  19504  efginvrel2  19721  efginvrel1  19722  efgsp1  19731  efgsres  19732  efgsfo  19733  frgpinv  19758  frgpupf  19767  frgpup1  19769  subcmn  19831  torsubg  19848  dprd2dlem1  20037  dpjidcl  20054  ablfaclem3  20083  nzrring  20494  lringnzr  20519  fldhmsubc  20760  acsfn1p  20774  lssacs  20940  cnsubdrglem  21411  rege0subm  21416  rge0srg  21431  zringunit  21452  znrrg  21559  psgnghm  21572  zrhpsgnevpm  21583  evpmodpmf1o  21588  pmtrodpm  21589  phlssphl  21651  frlmsslsp  21790  islinds4  21829  lmimlbs  21830  lbslcic  21835  psrbaglefi  21925  psrbaglefiOLD  21926  psrbagconf1o  21930  mplsubglem  22004  mplneg  22015  ressmpladd  22032  ressmplmul  22033  ressmplvsca  22034  mplmonmul  22039  psdmul  22156  ply1bascl  22189  mdetralt  22598  mdetunilem7  22608  chfacfpmmulgsum2  22855  tgval2  22947  ordtbas  23184  ordtrestixx  23214  hauslly  23484  kgentop  23534  ptbasin  23569  filunirn  23874  uzrest  23889  elflim  23963  flffval  23981  fclsval  24000  isfcls  24001  fcfval  24025  ustn0  24213  fmucndlem  24284  xmetunirn  24331  mopnval  24432  setsmstopn  24474  tmsval  24477  tngtopn  24655  qtopbaslem  24763  xrtgioo  24810  reperflem  24822  icccmplem1  24826  icopnfhmeo  24956  icccvx  24963  bndth  24972  reparphtiOLD  25012  pcoval1  25028  pcoval2  25031  pcoass  25039  pcorevlem  25041  pcorev2  25043  pi1xfrcnv  25072  csscld  25265  cfilfval  25280  caufval  25291  bcthlem1  25340  ivthlem1  25468  ivthlem3  25470  ovolicc2lem3  25536  ovolicc2lem4  25537  vitalilem1  25625  mbflimsup  25683  i1fd  25698  i1f0  25704  i1f1  25707  itg1addlem4  25716  itg1addlem4OLD  25717  itg1addlem5  25718  iblmbf  25785  ellimc2  25894  limcres  25903  limcun  25912  dvbsss  25919  perfdvf  25920  dvres2lem  25927  dvaddbr  25956  rolle  26010  cmvth  26011  cmvthOLD  26012  dvlip  26014  dvlipcn  26015  dvle  26028  lhop1lem  26034  dvfsumle  26042  dvfsumleOLD  26043  dvfsumge  26044  dvfsumabs  26045  dvfsumlem2  26049  dvfsumlem2OLD  26050  ftc2  26067  itgparts  26070  itgsubstlem  26071  itgsubst  26072  deg1mul3  26140  coeval  26247  coeeu  26249  dgrval  26252  coef3  26256  coemulc  26279  dgrsub  26297  coecj  26303  dvply2  26311  dvnply  26313  quotval  26317  fta1  26333  plyexmo  26338  aacjcl  26352  taylfval  26383  dvtaylp  26395  abelth  26468  pilem3  26480  cos0pilt1  26556  sinord  26558  recosf1o  26559  resinf1o  26560  tanord1  26561  eff1olem  26572  dvloglem  26672  dvlog  26675  dvlog2lem  26676  advlogexp  26679  logtayl  26684  logtayl2  26686  dvcncxp1  26767  dvcnsqrt  26768  cxpcn3lem  26772  cxpcn3  26773  sqrtcn  26775  loglesqrt  26786  1cubr  26867  acosrecl  26928  efrlim  26994  efrlimOLD  26995  jensen  27014  lgamgulmlem2  27055  lgamucov2  27064  basellem4  27109  musum  27216  mpodvdsmulf1o  27219  fsumdvdsmul  27220  dchrinvcl  27279  dchrghm  27282  dchrinv  27287  dchrsum2  27294  dchrsum  27295  rpvmasumlem  27513  dchrisum0lem2a  27543  pnt  27640  oldf  27878  leftirr  27911  rightirr  27912  lrold  27917  sltlpss  27927  addsproplem2  27981  sleadd1  28000  addsuniflem  28012  negsproplem2  28035  negsid  28047  negsunif  28061  mulsrid  28111  mulsproplem12  28125  mulsproplem13  28126  mulsproplem14  28127  precsexlem9  28211  precsexlem11  28213  onsno  28246  n0sno  28293  nnsno  28294  nnn0s  28297  nnsgt0  28307  zno  28329  tglng  28470  axlowdimlem6  28878  axlowdimlem16  28888  axlowdimlem17  28889  axlowdim  28892  axeuclidlem  28893  axcontlem2  28896  axcontlem7  28901  axcontlem8  28902  nbusgrvtxm1uvtx  29338  wlk1walk  29573  pthdivtx  29663  pthdadjvtx  29664  crctcshwlkn0lem2  29742  crctcshwlkn0lem4  29744  clwwisshclwws  29945  fusgreg2wsp  30266  nvvcop  30524  nvex  30541  phnv  30744  sheli  31144  cheli  31162  hhssabloilem  31191  choc1  31257  shintcli  31259  chintcli  31261  shsleji  31300  pjini  31629  mayete3i  31658  dmadjop  31818  nlelshi  31990  cnlnadjeui  32007  cnlnssadj  32010  bdopadj  32012  pjimai  32106  stcl  32146  atelch  32274  fcnvgreu  32590  f1od2  32635  fcobijfs  32637  uzssico  32689  iundisj2fi  32702  nnindf  32723  eliccioo  32795  gsummptres  32924  cyc3genpm  33034  elrspunidl  33309  zarcls  33702  ordtrestNEW  33749  xrge0iifcnv  33761  xrge0iifcv  33762  xrge0iifiso  33763  xrge0iifhom  33765  qqhcn  33819  esumval  33892  gsumesum  33905  esumlub  33906  esumcst  33909  esumfsup  33916  issgon  33969  elrnsiga  33972  imambfm  34109  br2base  34116  sxbrsigalem0  34118  dya2iocucvr  34131  sxbrsigalem2  34133  sxbrsigalem5  34135  sxbrsiga  34137  omssubadd  34147  sitmcl  34198  oddpwdc  34201  eulerpartlemelr  34204  eulerpartlemgvv  34223  eulerpartlemgh  34225  eulerpartlemgs2  34227  eulerpartlemn  34228  sseqf  34239  ballotlem2  34335  ballotlemfp1  34338  ballotlemfc0  34339  ballotlemfcc  34340  ballotlemfmpn  34341  ballotlemsup  34351  ballotlemfrceq  34375  signswch  34420  rpsqrtcn  34452  prodfzo03  34462  itgexpif  34465  bnj1533  34710  bnj1137  34853  bnj1286  34877  bnj1408  34894  bnj1417  34899  subfacp1lem5  35025  cvmsi  35106  gonar  35236  goalr  35238  mpst123  35381  mpstrcl  35382  msrrcl  35384  elmsta  35389  msubvrs  35401  elmpps  35414  elmthm  35417  bcprod  35573  dfon2lem4  35623  pprodss4v  35721  ivthALT  36060  neibastop2lem  36085  nnssi2  36180  nnssi3  36181  bj-sngltagi  36702  bj-elid5  36889  bj-fvmptunsn1  36977  bj-smgrpssmgmel  36989  bj-mndsssmgrpel  36991  bj-cmnssmndel  36993  bj-grpssmndel  36995  bj-ablssgrpel  36997  bj-ablsscmnel  36999  bj-vecssmodel  37002  bj-flddrng  37009  bj-rveccvec  37025  bj-rvecabl  37027  taupilemrplb  37040  icorempo  37071  elxp8  37091  sin2h  37324  cos2h  37325  tan2h  37326  poimirlem14  37348  poimirlem26  37360  poimirlem27  37361  poimirlem31  37365  poimirlem32  37366  mblfinlem1  37371  cnambfre  37382  dvtan  37384  itg2addnc  37388  itg2gt0cn  37389  ftc1cnnc  37406  ftc2nc  37416  dvasin  37418  dvacos  37419  cover2  37429  sstotbnd2  37488  heibor1lem  37523  heiborlem10  37534  opidonOLD  37566  exidcl  37590  rngosn3  37638  flddivrng  37713  toycom  38684  osumcllem7N  39674  pexmidlem4N  39685  diaintclN  40770  dibintclN  40879  mapd1o  41360  hdmapevec  41547  dvrelog2  41776  aks6d1c2lem4  41839  sticksstones1  41858  aks6d1c6lem5  41889  imacrhmcl  42204  prjspvs  42300  prjspeclsp  42302  0prjspnrel  42317  elrfi  42388  elrfirn  42389  elrfirn2  42390  mrefg3  42402  diophin  42466  diophun  42467  eq0rabdioph  42470  eqrabdioph  42471  pellex  42529  rmxycomplete  42612  jm2.23  42691  aomclem2  42753  fglmod  42771  lsmfgcl  42772  lmhmfgima  42782  lmhmfgsplit  42784  isnumbasabl  42804  dgrsub2  42833  itgocn  42862  areaquad  42918  cantnftermord  43023  omabs2  43035  nna1iscard  43249  elmapintrab  43280  corcltrcl  43443  k0004val0  43858  elscottab  43955  radcnvrat  44025  uzmptshftfval  44057  binomcxplemdvsum  44066  binomcxplemnotnn0  44067  onfrALTlem2  44259  onfrALTlem2VD  44602  uzwo4  44691  mptssid  44885  uzublem  45081  eliccelioc  45175  elicores  45187  sqrlearg  45207  fsumiunss  45232  limcdm0  45275  sumnnodd  45287  fnlimfvre  45331  limsupubuzlem  45369  limsupmnflem  45377  limsupre3uzlem  45392  climuzlem  45400  cncfshift  45531  cncfperiod  45536  icccncfext  45544  dvnprodlem1  45603  dvnprodlem2  45604  itgsin0pilem1  45607  itgsinexplem1  45611  itgsinexp  45612  ditgeqiooicc  45617  itgsubsticclem  45632  itgioocnicc  45634  itgsbtaddcnst  45639  stoweidlem34  45691  stoweidlem41  45698  stoweidlem51  45708  wallispilem2  45723  stirlinglem11  45741  dirkercncflem2  45761  fourierdlem5  45769  fourierdlem9  45773  fourierdlem17  45781  fourierdlem18  45782  fourierdlem20  45784  fourierdlem39  45803  fourierdlem48  45811  fourierdlem49  45812  fourierdlem62  45825  fourierdlem66  45829  fourierdlem68  45831  fourierdlem72  45835  fourierdlem73  45836  fourierdlem81  45844  fourierdlem83  45846  fourierdlem85  45848  fourierdlem87  45850  fourierdlem88  45851  fourierdlem92  45855  fourierdlem95  45858  fourierdlem103  45866  fourierdlem104  45867  fourierdlem112  45875  sqwvfoura  45885  sqwvfourb  45886  fouriersw  45888  etransclem24  45915  etransclem35  45926  etransclem37  45928  salexct  45991  salgencntex  46000  sge0resplit  46063  sge0split  46066  meaiuninclem  46137  caratheodorylem1  46183  volicorescl  46210  hoidmv1lelem3  46250  opnvonmbllem2  46290  ovolval2  46301  ovolval3  46304  ovolval4lem1  46306  ovolval4lem2  46307  pimiooltgt  46367  sssmf  46395  smfaddlem1  46420  smflimlem2  46429  smfrec  46446  smfdiv  46454  smfsuplem1  46468  smfsuplem3  46470  et-ltneverrefl  46528  natglobalincr  46532  fcores  46718  spr0el  47090  bgoldbtbndlem2  47414  bgoldbtbndlem3  47415  bgoldbtbnd  47417  fldhmsubcALTV  47746  fvconst0ci  48262  fvconstdomi  48263