Theorem sseli 3931

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3920

This theorem is referenced by:  sselii  3932  sselid  3933  elun1  4133  elun2  4134  elopabr  5503  elopabran  5504  elopaelxp  5709  copsex2ga  5750  2elresin  6603  nfvres  6861  fvco4i  6924  mptrcl  6939  fvmptss  6942  fvmptex  6944  fvmptnf  6952  elfvmptrab1w  6957  elfvmptrab1  6958  fvopab4ndm  6960  fvimacnvi  6986  elpreima  6992  iinpreima  7003  ofrfvalg  7621  ofval  7624  off  7631  nnon  7805  finds  7829  finds2  7831  eqopi  7960  op1steq  7968  dfoprab4  7990  bropopvvv  8023  bropfvvvv  8025  reldmtpos  8167  smores2  8277  frsuc  8359  unifpw  9245  cantnfp1lem1  9574  cantnfp1lem3  9576  r1fin  9669  r1tr  9672  r1ordg  9674  r1ord3g  9675  r1val1  9682  tz9.12lem3  9685  tcrank  9780  cplem1  9785  hta  9793  tskwe  9846  cardprclem  9875  alephfplem3  10000  dfac12r  10041  ackbij1lem16  10128  ackbij2  10136  fin23lem28  10234  fin23lem30  10236  fin23lem31  10237  fin1a2lem6  10299  hsmexlem4  10323  hsmexlem5  10324  hsmexlem6  10325  axdc2lem  10342  axdc3lem2  10345  axcclem  10351  brdom5  10423  brdom4  10424  r1tskina  10676  gruina  10712  grur1a  10713  pinn  10772  0nnq  10818  elpqn  10819  recn  11099  rexr  11161  ltord1  11646  leord1  11647  eqord1  11648  nnre  12135  nncn  12136  nnind  12146  nnnn0  12391  nn0re  12393  nn0cn  12394  nn0xnn0  12461  nnzOLD  12495  nn0z  12496  uzuzle35  12788  nnq  12863  qcn  12864  rpre  12902  eliccxr  13338  difreicc  13387  iccshftri  13390  iccshftli  13392  iccdili  13394  icccntri  13396  fzval2  13413  fzelp1  13479  4fvwrd4  13551  elfzo1  13615  ico01fl0  13723  expcllem  13979  expcl2lem  13980  m1expcl2  13992  bcm1k  14222  bcpasc  14228  hashbclem  14359  wrdv  14436  pfxfv0  14598  pfxfvlsw  14601  cshimadifsn  14736  swrds2m  14848  01sqrexlem5  15153  cau3lem  15262  caubnd  15266  climconst2  15455  o1of2  15520  o1rlimmul  15526  caurcvg  15584  caucvg  15586  binomlem  15736  incexclem  15743  divcnvshft  15762  zprod  15844  fprodge1  15902  risefaccllem  15920  fallfaccllem  15921  bpolydiflem  15961  bpoly4  15966  dvdsflip  16228  divalglem8  16311  sadadd  16378  smumul  16404  isprm3  16594  phimullem  16690  prmdiveq  16697  unbenlem  16820  vdwnnlem1  16907  vdwnnlem3  16909  ramtcl2  16923  prmgaplem4  16966  cshwshashlem1  17007  structcnvcnv  17064  fvsetsid  17079  imasdsval2  17420  mreunirn  17503  mrcfval  17514  mrisval  17536  coapm  17978  tsrss  18495  submnd0  18637  smndex1id  18785  nmzsubg  19044  nmznsg  19047  cntzmhm  19220  symgtrinv  19351  pmtrdifellem4  19358  psgnpmtr  19389  efginvrel2  19606  efginvrel1  19607  efgsp1  19616  efgsres  19617  efgsfo  19618  frgpinv  19643  frgpupf  19652  frgpup1  19654  subcmn  19716  torsubg  19733  dprd2dlem1  19922  dpjidcl  19939  ablfaclem3  19968  nzrring  20401  lringnzr  20426  fldhmsubc  20670  acsfn1p  20684  lssacs  20870  cnsubdrglem  21325  rege0subm  21330  rge0srg  21345  zringunit  21373  znrrg  21472  psgnghm  21487  zrhpsgnevpm  21498  evpmodpmf1o  21503  pmtrodpm  21504  phlssphl  21566  frlmsslsp  21703  islinds4  21742  lmimlbs  21743  lbslcic  21748  psrbaglefi  21833  psrbagconf1o  21836  mplsubglem  21906  mplneg  21917  ressmpladd  21934  ressmplmul  21935  ressmplvsca  21936  mplmonmul  21941  psdmul  22051  ply1bascl  22086  mdetralt  22493  mdetunilem7  22503  chfacfpmmulgsum2  22750  tgval2  22841  ordtbas  23077  ordtrestixx  23107  hauslly  23377  kgentop  23427  ptbasin  23462  filunirn  23767  uzrest  23782  elflim  23856  flffval  23874  fclsval  23893  isfcls  23894  fcfval  23918  ustn0  24106  fmucndlem  24176  xmetunirn  24223  mopnval  24324  setsmstopn  24364  tmsval  24367  tngtopn  24536  qtopbaslem  24644  xrtgioo  24693  reperflem  24705  icccmplem1  24709  icopnfhmeo  24839  icccvx  24846  bndth  24855  reparphtiOLD  24895  pcoval1  24911  pcoval2  24914  pcoass  24922  pcorevlem  24924  pcorev2  24926  pi1xfrcnv  24955  csscld  25147  cfilfval  25162  caufval  25173  bcthlem1  25222  ivthlem1  25350  ivthlem3  25352  ovolicc2lem3  25418  ovolicc2lem4  25419  vitalilem1  25507  mbflimsup  25565  i1fd  25580  i1f0  25586  i1f1  25589  itg1addlem4  25598  itg1addlem5  25599  iblmbf  25666  ellimc2  25776  limcres  25785  limcun  25794  dvbsss  25801  perfdvf  25802  dvres2lem  25809  dvaddbr  25838  rolle  25892  cmvth  25893  cmvthOLD  25894  dvlip  25896  dvlipcn  25897  dvle  25910  lhop1lem  25916  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  ftc2  25949  itgparts  25952  itgsubstlem  25953  itgsubst  25954  deg1mul3  26019  coeval  26126  coeeu  26128  dgrval  26131  coef3  26135  coemulc  26158  dgrsub  26176  coecj  26182  coecjOLD  26184  dvply2  26192  dvnply  26194  quotval  26198  fta1  26214  plyexmo  26219  aacjcl  26233  taylfval  26264  dvtaylp  26276  abelth  26349  pilem3  26361  cos0pilt1  26439  sinord  26441  recosf1o  26442  resinf1o  26443  tanord1  26444  eff1olem  26455  dvloglem  26555  dvlog  26558  dvlog2lem  26559  advlogexp  26562  logtayl  26567  logtayl2  26569  dvcncxp1  26650  dvcnsqrt  26651  cxpcn3lem  26655  cxpcn3  26656  sqrtcn  26658  loglesqrt  26669  1cubr  26750  acosrecl  26811  efrlim  26877  efrlimOLD  26878  jensen  26897  lgamgulmlem2  26938  lgamucov2  26947  basellem4  26992  musum  27099  mpodvdsmulf1o  27102  fsumdvdsmul  27103  dchrinvcl  27162  dchrghm  27165  dchrinv  27170  dchrsum2  27177  dchrsum  27178  rpvmasumlem  27396  dchrisum0lem2a  27426  pnt  27523  oldf  27767  leftirr  27805  rightirr  27806  lrold  27811  newbdayim  27817  sltlpss  27822  addsproplem2  27882  sleadd1  27901  addsuniflem  27913  addsbdaylem  27928  addsbday  27929  negsproplem2  27940  negsid  27952  negsunif  27966  mulsrid  28021  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  precsexlem9  28122  precsexlem11  28124  onsno  28161  onscutlt  28170  onaddscl  28179  onmulscl  28180  n0sno  28221  nnsno  28222  nnn0s  28225  nnsgt0  28236  zno  28275  expscllem  28322  tglng  28491  axlowdimlem6  28892  axlowdimlem16  28902  axlowdimlem17  28903  axlowdim  28906  axeuclidlem  28907  axcontlem2  28910  axcontlem7  28915  axcontlem8  28916  nbusgrvtxm1uvtx  29350  wlk1walk  29584  pthdivtx  29672  pthdadjvtx  29673  crctcshwlkn0lem2  29756  crctcshwlkn0lem4  29758  clwwisshclwws  29959  fusgreg2wsp  30280  nvvcop  30538  nvex  30555  phnv  30758  sheli  31158  cheli  31176  hhssabloilem  31205  choc1  31271  shintcli  31273  chintcli  31275  shsleji  31314  pjini  31643  mayete3i  31672  dmadjop  31832  nlelshi  32004  cnlnadjeui  32021  cnlnssadj  32024  bdopadj  32026  pjimai  32120  stcl  32160  atelch  32288  fcnvgreu  32616  f1od2  32663  fcobijfs  32665  fcobijfs2  32666  uzssico  32727  iundisj2fi  32740  nnindf  32764  eliccioo  32871  gsummptres  33005  cyc3genpm  33094  elrspunidl  33365  zarcls  33841  ordtrestNEW  33888  xrge0iifcnv  33900  xrge0iifcv  33901  xrge0iifiso  33902  xrge0iifhom  33904  qqhcn  33958  esumval  34013  gsumesum  34026  esumlub  34027  esumcst  34030  esumfsup  34037  issgon  34090  elrnsiga  34093  imambfm  34230  br2base  34237  sxbrsigalem0  34239  dya2iocucvr  34252  sxbrsigalem2  34254  sxbrsigalem5  34256  sxbrsiga  34258  omssubadd  34268  sitmcl  34319  oddpwdc  34322  eulerpartlemelr  34325  eulerpartlemgvv  34344  eulerpartlemgh  34346  eulerpartlemgs2  34348  eulerpartlemn  34349  sseqf  34360  ballotlem2  34457  ballotlemfp1  34460  ballotlemfc0  34461  ballotlemfcc  34462  ballotlemfmpn  34463  ballotlemsup  34473  ballotlemfrceq  34497  signswch  34529  rpsqrtcn  34561  prodfzo03  34571  itgexpif  34574  bnj1533  34819  bnj1137  34962  bnj1286  34986  bnj1408  35003  bnj1417  35008  onvf1odlem4  35079  subfacp1lem5  35157  cvmsi  35238  gonar  35368  goalr  35370  mpst123  35513  mpstrcl  35514  msrrcl  35516  elmsta  35521  msubvrs  35533  elmpps  35546  elmthm  35549  bcprod  35711  dfon2lem4  35760  pprodss4v  35858  ivthALT  36309  neibastop2lem  36334  nnssi2  36429  nnssi3  36430  bj-sngltagi  36956  bj-elid5  37143  bj-fvmptunsn1  37231  bj-smgrpssmgmel  37243  bj-mndsssmgrpel  37245  bj-cmnssmndel  37247  bj-grpssmndel  37249  bj-ablssgrpel  37251  bj-ablsscmnel  37253  bj-vecssmodel  37256  bj-flddrng  37263  bj-rveccvec  37279  bj-rvecabl  37281  taupilemrplb  37294  icorempo  37325  elxp8  37345  sin2h  37590  cos2h  37591  tan2h  37592  poimirlem14  37614  poimirlem26  37626  poimirlem27  37627  poimirlem31  37631  poimirlem32  37632  mblfinlem1  37637  cnambfre  37648  dvtan  37650  itg2addnc  37654  itg2gt0cn  37655  ftc1cnnc  37672  ftc2nc  37682  dvasin  37684  dvacos  37685  cover2  37695  sstotbnd2  37754  heibor1lem  37789  heiborlem10  37800  opidonOLD  37832  exidcl  37856  rngosn3  37904  flddivrng  37979  toycom  38952  osumcllem7N  39941  pexmidlem4N  39952  diaintclN  41037  dibintclN  41146  mapd1o  41627  hdmapevec  41814  dvrelog2  42037  aks6d1c2lem4  42100  sticksstones1  42119  aks6d1c6lem5  42150  redvmptabs  42333  imacrhmcl  42487  prjspvs  42583  prjspeclsp  42585  0prjspnrel  42600  elrfi  42667  elrfirn  42668  elrfirn2  42669  mrefg3  42681  diophin  42745  diophun  42746  eq0rabdioph  42749  eqrabdioph  42750  pellex  42808  rmxycomplete  42890  jm2.23  42969  aomclem2  43028  fglmod  43046  lsmfgcl  43047  lmhmfgima  43057  lmhmfgsplit  43059  isnumbasabl  43079  dgrsub2  43108  itgocn  43137  areaquad  43189  cantnftermord  43293  omabs2  43305  nna1iscard  43518  elmapintrab  43549  corcltrcl  43712  k0004val0  44127  elscottab  44217  radcnvrat  44287  uzmptshftfval  44319  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  onfrALTlem2  44520  onfrALTlem2VD  44862  uzwo4  45031  mptssid  45219  uzublem  45409  eliccelioc  45502  elicores  45514  sqrlearg  45534  fsumiunss  45556  limcdm0  45599  sumnnodd  45611  fnlimfvre  45655  limsupubuzlem  45693  limsupmnflem  45701  limsupre3uzlem  45716  climuzlem  45724  liminflelimsuplem  45756  cncfshift  45855  cncfperiod  45860  icccncfext  45868  dvnprodlem1  45927  dvnprodlem2  45928  itgsin0pilem1  45931  itgsinexplem1  45935  itgsinexp  45936  ditgeqiooicc  45941  itgsubsticclem  45956  itgioocnicc  45958  itgsbtaddcnst  45963  stoweidlem34  46015  stoweidlem41  46022  stoweidlem51  46032  wallispilem2  46047  stirlinglem11  46065  dirkercncflem2  46085  fourierdlem5  46093  fourierdlem9  46097  fourierdlem17  46105  fourierdlem18  46106  fourierdlem20  46108  fourierdlem39  46127  fourierdlem48  46135  fourierdlem49  46136  fourierdlem62  46149  fourierdlem66  46153  fourierdlem68  46155  fourierdlem72  46159  fourierdlem73  46160  fourierdlem81  46168  fourierdlem83  46170  fourierdlem85  46172  fourierdlem87  46174  fourierdlem88  46175  fourierdlem92  46179  fourierdlem95  46182  fourierdlem103  46190  fourierdlem104  46191  fourierdlem112  46199  sqwvfoura  46209  sqwvfourb  46210  fouriersw  46212  etransclem24  46239  etransclem35  46250  etransclem37  46252  salexct  46315  salgencntex  46324  sge0resplit  46387  sge0split  46390  meaiuninclem  46461  caratheodorylem1  46507  volicorescl  46534  hoidmv1lelem3  46574  opnvonmbllem2  46614  ovolval2  46625  ovolval3  46628  ovolval4lem1  46630  ovolval4lem2  46631  pimiooltgt  46691  sssmf  46719  smfaddlem1  46744  smflimlem2  46753  smfrec  46770  smfdiv  46778  smfsuplem1  46792  smfsuplem3  46794  et-ltneverrefl  46852  natglobalincr  46858  tannpoly  46874  fcores  47051  rehalfge1  47319  spr0el  47466  bgoldbtbndlem2  47790  bgoldbtbndlem3  47791  bgoldbtbnd  47793  upgrimpthslem2  47892  stgredgiun  47942  isubgr3stgrlem7  47956  fldhmsubcALTV  48317  fvconst0ci  48875  fvconstdomi  48876  idfullsubc  49146  fulloppf  49148  fthoppf  49149  initopropdlemlem  49224