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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890

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 2812  df-ss 3907

This theorem is referenced by:  sselii  3919  sselid  3920  elun1  4123  elun2  4124  elopabr  5509  elopabran  5510  elopaelxp  5715  copsex2ga  5757  2elresin  6614  nfvres  6873  fvco4i  6936  mptrcl  6952  fvmptss  6955  fvmptex  6957  fvmptnf  6965  elfvmptrab1w  6970  elfvmptrab1  6971  fvopab4ndm  6973  fvimacnvi  6999  elpreima  7005  iinpreima  7016  ofrfvalg  7633  ofval  7636  off  7643  nnon  7817  finds  7841  finds2  7843  eqopi  7972  op1steq  7980  dfoprab4  8002  bropopvvv  8034  bropfvvvv  8036  reldmtpos  8178  smores2  8288  frsuc  8370  unifpw  9259  cantnfp1lem1  9593  cantnfp1lem3  9595  r1fin  9691  r1tr  9694  r1ordg  9696  r1ord3g  9697  r1val1  9704  tz9.12lem3  9707  tcrank  9802  cplem1  9807  hta  9815  tskwe  9868  cardprclem  9897  alephfplem3  10022  dfac12r  10063  ackbij1lem16  10150  ackbij2  10158  fin23lem28  10256  fin23lem30  10258  fin23lem31  10259  fin1a2lem6  10321  hsmexlem4  10345  hsmexlem5  10346  hsmexlem6  10347  axdc2lem  10364  axdc3lem2  10367  axcclem  10373  brdom5  10445  brdom4  10446  r1tskina  10699  gruina  10735  grur1a  10736  pinn  10795  0nnq  10841  elpqn  10842  recn  11122  rexr  11185  ltord1  11670  leord1  11671  eqord1  11672  nnre  12175  nncn  12176  nnind  12186  nnnn0  12438  nn0re  12440  nn0cn  12441  nn0xnn0  12508  nn0z  12542  uzuzle35  12831  nnq  12906  qcn  12907  rpre  12945  eliccxr  13382  difreicc  13431  iccshftri  13434  iccshftli  13436  iccdili  13438  icccntri  13440  fzval2  13458  fzelp1  13524  4fvwrd4  13596  elfzo1  13661  ico01fl0  13772  expcllem  14028  expcl2lem  14029  m1expcl2  14041  bcm1k  14271  bcpasc  14277  hashbclem  14408  wrdv  14485  pfxfv0  14648  pfxfvlsw  14651  cshimadifsn  14785  swrds2m  14897  01sqrexlem5  15202  cau3lem  15311  caubnd  15315  climconst2  15504  o1of2  15569  o1rlimmul  15575  caurcvg  15633  caucvg  15635  binomlem  15788  incexclem  15795  divcnvshft  15814  zprod  15896  fprodge1  15954  risefaccllem  15972  fallfaccllem  15973  bpolydiflem  16013  bpoly4  16018  dvdsflip  16280  divalglem8  16363  sadadd  16430  smumul  16456  isprm3  16646  phimullem  16743  prmdiveq  16750  unbenlem  16873  vdwnnlem1  16960  vdwnnlem3  16962  ramtcl2  16976  prmgaplem4  17019  cshwshashlem1  17060  structcnvcnv  17117  fvsetsid  17132  imasdsval2  17474  mreunirn  17557  mrcfval  17568  mrisval  17590  coapm  18032  tsrss  18549  chnccat  18586  ex-chn1  18597  submnd0  18725  smndex1id  18876  nmzsubg  19134  nmznsg  19137  cntzmhm  19310  symgtrinv  19441  pmtrdifellem4  19448  psgnpmtr  19479  efginvrel2  19696  efginvrel1  19697  efgsp1  19706  efgsres  19707  efgsfo  19708  frgpinv  19733  frgpupf  19742  frgpup1  19744  subcmn  19806  torsubg  19823  dprd2dlem1  20012  dpjidcl  20029  ablfaclem3  20058  nzrring  20487  lringnzr  20512  fldhmsubc  20756  acsfn1p  20770  lssacs  20956  cnsubdrglem  21411  rege0subm  21416  rge0srg  21431  zringunit  21459  znrrg  21558  psgnghm  21573  zrhpsgnevpm  21584  evpmodpmf1o  21589  pmtrodpm  21590  phlssphl  21652  frlmsslsp  21789  islinds4  21828  lmimlbs  21829  lbslcic  21834  psrbaglefi  21919  psrbagconf1o  21922  mplsubglem  21990  mplneg  22001  ressmpladd  22020  ressmplmul  22021  ressmplvsca  22022  mplmonmul  22027  psdmul  22145  ply1bascl  22180  mdetralt  22586  mdetunilem7  22596  chfacfpmmulgsum2  22843  tgval2  22934  ordtbas  23170  ordtrestixx  23200  hauslly  23470  kgentop  23520  ptbasin  23555  filunirn  23860  uzrest  23875  elflim  23949  flffval  23967  fclsval  23986  isfcls  23987  fcfval  24011  ustn0  24199  fmucndlem  24268  xmetunirn  24315  mopnval  24416  setsmstopn  24456  tmsval  24459  tngtopn  24628  qtopbaslem  24736  xrtgioo  24785  reperflem  24797  icccmplem1  24801  icopnfhmeo  24923  icccvx  24930  bndth  24938  pcoval1  24993  pcoval2  24996  pcoass  25004  pcorevlem  25006  pcorev2  25008  pi1xfrcnv  25037  csscld  25229  cfilfval  25244  caufval  25255  bcthlem1  25304  ivthlem1  25431  ivthlem3  25433  ovolicc2lem3  25499  ovolicc2lem4  25500  vitalilem1  25588  mbflimsup  25646  i1fd  25661  i1f0  25667  i1f1  25670  itg1addlem4  25679  itg1addlem5  25680  iblmbf  25747  ellimc2  25857  limcres  25866  limcun  25875  dvbsss  25882  perfdvf  25883  dvres2lem  25890  dvaddbr  25918  rolle  25970  cmvth  25971  dvlip  25973  dvlipcn  25974  dvle  25987  lhop1lem  25993  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  dvfsumlem2  26007  ftc2  26024  itgparts  26027  itgsubstlem  26028  itgsubst  26029  deg1mul3  26094  coeval  26201  coeeu  26203  dgrval  26206  coef3  26210  coemulc  26233  dgrsub  26250  coecj  26256  coecjOLD  26258  dvply2  26266  dvnply  26268  quotval  26272  fta1  26288  plyexmo  26293  aacjcl  26307  taylfval  26338  dvtaylp  26350  abelth  26422  pilem3  26434  cos0pilt1  26512  sinord  26514  recosf1o  26515  resinf1o  26516  tanord1  26517  eff1olem  26528  dvloglem  26628  dvlog  26631  dvlog2lem  26632  advlogexp  26635  logtayl  26640  logtayl2  26642  dvcncxp1  26723  dvcnsqrt  26724  cxpcn3lem  26727  cxpcn3  26728  sqrtcn  26730  loglesqrt  26741  1cubr  26822  acosrecl  26883  efrlim  26949  efrlimOLD  26950  jensen  26969  lgamgulmlem2  27010  lgamucov2  27019  basellem4  27064  musum  27171  mpodvdsmulf1o  27174  fsumdvdsmul  27175  dchrinvcl  27233  dchrghm  27236  dchrinv  27241  dchrsum2  27248  dchrsum  27249  rpvmasumlem  27467  dchrisum0lem2a  27497  pnt  27594  oldf  27846  madeno  27852  oldno  27853  newno  27854  oldmade  27877  leftold  27884  rightold  27885  leftno  27886  rightno  27887  addbdaylem  28026  addbday  28027  negsproplem2  28038  negsid  28050  negsunif  28064  mulsproplem12  28136  mulsproplem13  28137  mulsproplem14  28138  precsexlem11  28226  onno  28264  oncutlt  28273  n0no  28332  nnno  28333  nnn0s  28336  nnsgt0  28348  zno  28391  expscllem  28439  tglng  28631  axlowdimlem6  29033  axlowdimlem16  29043  axlowdimlem17  29044  axlowdim  29047  axeuclidlem  29048  axcontlem2  29051  axcontlem7  29056  axcontlem8  29057  nbusgrvtxm1uvtx  29491  wlk1walk  29725  pthdivtx  29813  pthdadjvtx  29814  crctcshwlkn0lem2  29897  crctcshwlkn0lem4  29899  clwwisshclwws  30103  fusgreg2wsp  30424  nvvcop  30683  nvex  30700  phnv  30903  sheli  31303  cheli  31321  hhssabloilem  31350  choc1  31416  shintcli  31418  chintcli  31420  shsleji  31459  pjini  31788  mayete3i  31817  dmadjop  31977  nlelshi  32149  cnlnadjeui  32166  cnlnssadj  32169  bdopadj  32171  pjimai  32265  stcl  32305  atelch  32433  fcnvgreu  32763  f1od2  32810  fcobijfs  32812  fcobijfs2  32813  uzssico  32875  iundisj2fi  32888  nnindf  32911  eliccioo  33008  gsummptres  33131  cyc3genpm  33231  elrspunidl  33506  psrmonmul  33712  zarcls  34037  ordtrestNEW  34084  xrge0iifcnv  34096  xrge0iifcv  34097  xrge0iifiso  34098  xrge0iifhom  34100  qqhcn  34154  esumval  34209  gsumesum  34222  esumlub  34223  esumcst  34226  esumfsup  34233  issgon  34286  elrnsiga  34289  imambfm  34425  br2base  34432  sxbrsigalem0  34434  dya2iocucvr  34447  sxbrsigalem2  34449  sxbrsigalem5  34451  sxbrsiga  34453  omssubadd  34463  sitmcl  34514  oddpwdc  34517  eulerpartlemelr  34520  eulerpartlemgvv  34539  eulerpartlemgh  34541  eulerpartlemgs2  34543  eulerpartlemn  34544  sseqf  34555  ballotlem2  34652  ballotlemfp1  34655  ballotlemfc0  34656  ballotlemfcc  34657  ballotlemfmpn  34658  ballotlemsup  34668  ballotlemfrceq  34692  signswch  34724  rpsqrtcn  34756  prodfzo03  34766  itgexpif  34769  bnj1533  35013  bnj1137  35156  bnj1286  35180  bnj1408  35197  bnj1417  35202  r1omhf  35268  onvf1odlem4  35307  subfacp1lem5  35385  cvmsi  35466  gonar  35596  goalr  35598  mpst123  35741  mpstrcl  35742  msrrcl  35744  elmsta  35749  msubvrs  35761  elmpps  35774  elmthm  35777  bcprod  35939  dfon2lem4  35985  pprodss4v  36083  ivthALT  36536  neibastop2lem  36561  nnssi2  36656  nnssi3  36657  ttcel2  36702  bj-sngltagi  37308  bj-elid5  37502  bj-fvmptunsn1  37590  bj-smgrpssmgmel  37602  bj-mndsssmgrpel  37604  bj-cmnssmndel  37606  bj-grpssmndel  37608  bj-ablssgrpel  37610  bj-ablsscmnel  37612  bj-vecssmodel  37615  bj-flddrng  37622  bj-rveccvec  37638  bj-rvecabl  37640  taupilemrplb  37653  icorempo  37684  elxp8  37704  sin2h  37948  cos2h  37949  tan2h  37950  poimirlem14  37972  poimirlem26  37984  poimirlem27  37985  poimirlem31  37989  poimirlem32  37990  mblfinlem1  37995  cnambfre  38006  dvtan  38008  itg2addnc  38012  itg2gt0cn  38013  ftc1cnnc  38030  ftc2nc  38040  dvasin  38042  dvacos  38043  cover2  38053  sstotbnd2  38112  heibor1lem  38147  heiborlem10  38158  opidonOLD  38190  exidcl  38214  rngosn3  38262  flddivrng  38337  toycom  39436  osumcllem7N  40425  pexmidlem4N  40436  diaintclN  41521  dibintclN  41630  mapd1o  42111  hdmapevec  42298  dvrelog2  42520  aks6d1c2lem4  42583  sticksstones1  42602  aks6d1c6lem5  42633  redvmptabs  42809  imacrhmcl  42976  prjspvs  43060  prjspeclsp  43062  0prjspnrel  43077  elrfi  43143  elrfirn  43144  elrfirn2  43145  mrefg3  43157  diophin  43221  diophun  43222  eq0rabdioph  43225  eqrabdioph  43226  pellex  43284  rmxycomplete  43366  jm2.23  43445  aomclem2  43504  fglmod  43522  lsmfgcl  43523  lmhmfgima  43533  lmhmfgsplit  43535  isnumbasabl  43555  dgrsub2  43584  itgocn  43613  areaquad  43665  cantnftermord  43769  omabs2  43781  nna1iscard  43993  elmapintrab  44024  corcltrcl  44187  k0004val0  44602  elscottab  44692  radcnvrat  44762  uzmptshftfval  44794  binomcxplemdvsum  44803  binomcxplemnotnn0  44804  onfrALTlem2  44994  onfrALTlem2VD  45336  uzwo4  45505  mptssid  45691  uzublem  45879  eliccelioc  45972  elicores  45984  sqrlearg  46004  fsumiunss  46026  limcdm0  46069  sumnnodd  46081  fnlimfvre  46123  limsupubuzlem  46161  limsupmnflem  46169  limsupre3uzlem  46184  climuzlem  46192  liminflelimsuplem  46224  cncfshift  46323  cncfperiod  46328  icccncfext  46336  dvnprodlem1  46395  dvnprodlem2  46396  itgsin0pilem1  46399  itgsinexplem1  46403  itgsinexp  46404  ditgeqiooicc  46409  itgsubsticclem  46424  itgioocnicc  46426  itgsbtaddcnst  46431  stoweidlem34  46483  stoweidlem41  46490  stoweidlem51  46500  wallispilem2  46515  stirlinglem11  46533  dirkercncflem2  46553  fourierdlem5  46561  fourierdlem9  46565  fourierdlem17  46573  fourierdlem18  46574  fourierdlem20  46576  fourierdlem39  46595  fourierdlem48  46603  fourierdlem49  46604  fourierdlem62  46617  fourierdlem66  46621  fourierdlem68  46623  fourierdlem72  46627  fourierdlem73  46628  fourierdlem81  46636  fourierdlem83  46638  fourierdlem85  46640  fourierdlem87  46642  fourierdlem88  46643  fourierdlem92  46647  fourierdlem95  46650  fourierdlem103  46658  fourierdlem104  46659  fourierdlem112  46667  sqwvfoura  46677  sqwvfourb  46678  fouriersw  46680  etransclem24  46707  etransclem35  46718  etransclem37  46720  salexct  46783  salgencntex  46792  sge0resplit  46855  sge0split  46858  meaiuninclem  46929  caratheodorylem1  46975  volicorescl  47002  hoidmv1lelem3  47042  opnvonmbllem2  47082  ovolval2  47093  ovolval3  47096  ovolval4lem1  47098  ovolval4lem2  47099  sssmf  47187  smfaddlem1  47212  smflimlem2  47221  smfrec  47238  smfdiv  47246  smfsuplem1  47260  smfsuplem3  47262  et-ltneverrefl  47320  natglobalincr  47326  tannpoly  47353  fcores  47530  elfz2nn  47785  rehalfge1  47802  spr0el  47957  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  upgrimpthslem2  48399  stgredgiun  48449  isubgr3stgrlem7  48463  fldhmsubcALTV  48824  fvconst0ci  49381  fvconstdomi  49382  idfullsubc  49651  fulloppf  49653  fthoppf  49654  initopropdlemlem  49729