Theorem sseli 3954

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926

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 2007  ax-8 2110

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

This theorem is referenced by:  sselii  3955  sselid  3956  elun1  4157  elun2  4158  elopabr  5536  elopabran  5537  elopaelxp  5744  copsex2ga  5786  2elresin  6658  nfvres  6916  fvco4i  6979  mptrcl  6994  fvmptss  6997  fvmptex  6999  fvmptnf  7007  elfvmptrab1w  7012  elfvmptrab1  7013  fvopab4ndm  7015  fvimacnvi  7041  elpreima  7047  iinpreima  7058  ofrfvalg  7677  ofval  7680  off  7687  nnon  7865  finds  7890  finds2  7892  eqopi  8022  op1steq  8030  dfoprab4  8052  bropopvvv  8087  bropfvvvv  8089  reldmtpos  8231  wfrlem10OLD  8330  smores2  8366  frsuc  8449  unifpw  9365  cantnfp1lem1  9690  cantnfp1lem3  9692  r1fin  9785  r1tr  9788  r1ordg  9790  r1ord3g  9791  r1val1  9798  tz9.12lem3  9801  tcrank  9896  cplem1  9901  hta  9909  tskwe  9962  cardprclem  9991  alephfplem3  10118  dfac12r  10159  ackbij1lem16  10246  ackbij2  10254  fin23lem28  10352  fin23lem30  10354  fin23lem31  10355  fin1a2lem6  10417  hsmexlem4  10441  hsmexlem5  10442  hsmexlem6  10443  axdc2lem  10460  axdc3lem2  10463  axcclem  10469  brdom5  10541  brdom4  10542  r1tskina  10794  gruina  10830  grur1a  10831  pinn  10890  0nnq  10936  elpqn  10937  recn  11217  rexr  11279  ltord1  11761  leord1  11762  eqord1  11763  nnre  12245  nncn  12246  nnind  12256  nnnn0  12506  nn0re  12508  nn0cn  12509  nn0xnn0  12576  nnzOLD  12610  nn0z  12611  nnq  12976  qcn  12977  rpre  13015  eliccxr  13450  difreicc  13499  iccshftri  13502  iccshftli  13504  iccdili  13506  icccntri  13508  fzval2  13525  fzelp1  13591  4fvwrd4  13663  elfzo1  13727  ico01fl0  13834  expcllem  14088  expcl2lem  14089  m1expcl2  14101  bcm1k  14331  bcpasc  14337  hashbclem  14468  wrdv  14545  pfxfv0  14708  pfxfvlsw  14711  cshimadifsn  14846  swrds2m  14958  01sqrexlem5  15263  cau3lem  15371  caubnd  15375  climconst2  15562  o1of2  15627  o1rlimmul  15633  caurcvg  15691  caucvg  15693  binomlem  15843  incexclem  15850  divcnvshft  15869  zprod  15951  fprodge1  16009  risefaccllem  16027  fallfaccllem  16028  bpolydiflem  16068  bpoly4  16073  dvdsflip  16334  divalglem8  16417  sadadd  16484  smumul  16510  isprm3  16700  phimullem  16796  prmdiveq  16803  unbenlem  16926  vdwnnlem1  17013  vdwnnlem3  17015  ramtcl2  17029  prmgaplem4  17072  cshwshashlem1  17113  structcnvcnv  17170  fvsetsid  17185  imasdsval2  17528  mreunirn  17611  mrcfval  17618  mrisval  17640  coapm  18082  tsrss  18597  submnd0  18739  smndex1id  18887  nmzsubg  19146  nmznsg  19149  cntzmhm  19322  symgtrinv  19451  pmtrdifellem4  19458  psgnpmtr  19489  efginvrel2  19706  efginvrel1  19707  efgsp1  19716  efgsres  19717  efgsfo  19718  frgpinv  19743  frgpupf  19752  frgpup1  19754  subcmn  19816  torsubg  19833  dprd2dlem1  20022  dpjidcl  20039  ablfaclem3  20068  nzrring  20474  lringnzr  20499  fldhmsubc  20743  acsfn1p  20757  lssacs  20922  cnsubdrglem  21384  rege0subm  21389  rge0srg  21404  zringunit  21425  znrrg  21524  psgnghm  21538  zrhpsgnevpm  21549  evpmodpmf1o  21554  pmtrodpm  21555  phlssphl  21617  frlmsslsp  21754  islinds4  21793  lmimlbs  21794  lbslcic  21799  psrbaglefi  21884  psrbagconf1o  21887  mplsubglem  21957  mplneg  21968  ressmpladd  21985  ressmplmul  21986  ressmplvsca  21987  mplmonmul  21992  psdmul  22102  ply1bascl  22137  mdetralt  22544  mdetunilem7  22554  chfacfpmmulgsum2  22801  tgval2  22892  ordtbas  23128  ordtrestixx  23158  hauslly  23428  kgentop  23478  ptbasin  23513  filunirn  23818  uzrest  23833  elflim  23907  flffval  23925  fclsval  23944  isfcls  23945  fcfval  23969  ustn0  24157  fmucndlem  24227  xmetunirn  24274  mopnval  24375  setsmstopn  24415  tmsval  24418  tngtopn  24587  qtopbaslem  24695  xrtgioo  24744  reperflem  24756  icccmplem1  24760  icopnfhmeo  24890  icccvx  24897  bndth  24906  reparphtiOLD  24946  pcoval1  24962  pcoval2  24965  pcoass  24973  pcorevlem  24975  pcorev2  24977  pi1xfrcnv  25006  csscld  25199  cfilfval  25214  caufval  25225  bcthlem1  25274  ivthlem1  25402  ivthlem3  25404  ovolicc2lem3  25470  ovolicc2lem4  25471  vitalilem1  25559  mbflimsup  25617  i1fd  25632  i1f0  25638  i1f1  25641  itg1addlem4  25650  itg1addlem5  25651  iblmbf  25718  ellimc2  25828  limcres  25837  limcun  25846  dvbsss  25853  perfdvf  25854  dvres2lem  25861  dvaddbr  25890  rolle  25944  cmvth  25945  cmvthOLD  25946  dvlip  25948  dvlipcn  25949  dvle  25962  lhop1lem  25968  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc2  26001  itgparts  26004  itgsubstlem  26005  itgsubst  26006  deg1mul3  26071  coeval  26178  coeeu  26180  dgrval  26183  coef3  26187  coemulc  26210  dgrsub  26228  coecj  26234  coecjOLD  26236  dvply2  26244  dvnply  26246  quotval  26250  fta1  26266  plyexmo  26271  aacjcl  26285  taylfval  26316  dvtaylp  26328  abelth  26401  pilem3  26413  cos0pilt1  26491  sinord  26493  recosf1o  26494  resinf1o  26495  tanord1  26496  eff1olem  26507  dvloglem  26607  dvlog  26610  dvlog2lem  26611  advlogexp  26614  logtayl  26619  logtayl2  26621  dvcncxp1  26702  dvcnsqrt  26703  cxpcn3lem  26707  cxpcn3  26708  sqrtcn  26710  loglesqrt  26721  1cubr  26802  acosrecl  26863  efrlim  26929  efrlimOLD  26930  jensen  26949  lgamgulmlem2  26990  lgamucov2  26999  basellem4  27044  musum  27151  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dchrinvcl  27214  dchrghm  27217  dchrinv  27222  dchrsum2  27229  dchrsum  27230  rpvmasumlem  27448  dchrisum0lem2a  27478  pnt  27575  oldf  27813  leftirr  27846  rightirr  27847  lrold  27852  sltlpss  27862  addsproplem2  27920  sleadd1  27939  addsuniflem  27951  addsbdaylem  27966  addsbday  27967  negsproplem2  27978  negsid  27990  negsunif  28004  mulsrid  28056  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  precsexlem9  28156  precsexlem11  28158  onsno  28195  onaddscl  28203  onmulscl  28204  n0sno  28245  nnsno  28246  nnn0s  28249  nnsgt0  28259  zno  28285  tglng  28471  axlowdimlem6  28872  axlowdimlem16  28882  axlowdimlem17  28883  axlowdim  28886  axeuclidlem  28887  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  nbusgrvtxm1uvtx  29330  wlk1walk  29565  pthdivtx  29655  pthdadjvtx  29656  crctcshwlkn0lem2  29739  crctcshwlkn0lem4  29741  clwwisshclwws  29942  fusgreg2wsp  30263  nvvcop  30521  nvex  30538  phnv  30741  sheli  31141  cheli  31159  hhssabloilem  31188  choc1  31254  shintcli  31256  chintcli  31258  shsleji  31297  pjini  31626  mayete3i  31655  dmadjop  31815  nlelshi  31987  cnlnadjeui  32004  cnlnssadj  32007  bdopadj  32009  pjimai  32103  stcl  32143  atelch  32271  fcnvgreu  32597  f1od2  32644  fcobijfs  32646  uzssico  32707  iundisj2fi  32720  nnindf  32744  eliccioo  32851  gsummptres  32992  cyc3genpm  33109  elrspunidl  33389  zarcls  33851  ordtrestNEW  33898  xrge0iifcnv  33910  xrge0iifcv  33911  xrge0iifiso  33912  xrge0iifhom  33914  qqhcn  33968  esumval  34023  gsumesum  34036  esumlub  34037  esumcst  34040  esumfsup  34047  issgon  34100  elrnsiga  34103  imambfm  34240  br2base  34247  sxbrsigalem0  34249  dya2iocucvr  34262  sxbrsigalem2  34264  sxbrsigalem5  34266  sxbrsiga  34268  omssubadd  34278  sitmcl  34329  oddpwdc  34332  eulerpartlemelr  34335  eulerpartlemgvv  34354  eulerpartlemgh  34356  eulerpartlemgs2  34358  eulerpartlemn  34359  sseqf  34370  ballotlem2  34467  ballotlemfp1  34470  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemfmpn  34473  ballotlemsup  34483  ballotlemfrceq  34507  signswch  34539  rpsqrtcn  34571  prodfzo03  34581  itgexpif  34584  bnj1533  34829  bnj1137  34972  bnj1286  34996  bnj1408  35013  bnj1417  35018  subfacp1lem5  35152  cvmsi  35233  gonar  35363  goalr  35365  mpst123  35508  mpstrcl  35509  msrrcl  35511  elmsta  35516  msubvrs  35528  elmpps  35541  elmthm  35544  bcprod  35701  dfon2lem4  35750  pprodss4v  35848  ivthALT  36299  neibastop2lem  36324  nnssi2  36419  nnssi3  36420  bj-sngltagi  36946  bj-elid5  37133  bj-fvmptunsn1  37221  bj-smgrpssmgmel  37233  bj-mndsssmgrpel  37235  bj-cmnssmndel  37237  bj-grpssmndel  37239  bj-ablssgrpel  37241  bj-ablsscmnel  37243  bj-vecssmodel  37246  bj-flddrng  37253  bj-rveccvec  37269  bj-rvecabl  37271  taupilemrplb  37284  icorempo  37315  elxp8  37335  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem14  37604  poimirlem26  37616  poimirlem27  37617  poimirlem31  37621  poimirlem32  37622  mblfinlem1  37627  cnambfre  37638  dvtan  37640  itg2addnc  37644  itg2gt0cn  37645  ftc1cnnc  37662  ftc2nc  37672  dvasin  37674  dvacos  37675  cover2  37685  sstotbnd2  37744  heibor1lem  37779  heiborlem10  37790  opidonOLD  37822  exidcl  37846  rngosn3  37894  flddivrng  37969  toycom  38937  osumcllem7N  39927  pexmidlem4N  39938  diaintclN  41023  dibintclN  41132  mapd1o  41613  hdmapevec  41800  dvrelog2  42023  aks6d1c2lem4  42086  sticksstones1  42105  aks6d1c6lem5  42136  redvmptabs  42350  imacrhmcl  42484  prjspvs  42580  prjspeclsp  42582  0prjspnrel  42597  elrfi  42664  elrfirn  42665  elrfirn2  42666  mrefg3  42678  diophin  42742  diophun  42743  eq0rabdioph  42746  eqrabdioph  42747  pellex  42805  rmxycomplete  42888  jm2.23  42967  aomclem2  43026  fglmod  43044  lsmfgcl  43045  lmhmfgima  43055  lmhmfgsplit  43057  isnumbasabl  43077  dgrsub2  43106  itgocn  43135  areaquad  43187  cantnftermord  43291  omabs2  43303  nna1iscard  43516  elmapintrab  43547  corcltrcl  43710  k0004val0  44125  elscottab  44216  radcnvrat  44286  uzmptshftfval  44318  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  onfrALTlem2  44519  onfrALTlem2VD  44861  uzwo4  45025  mptssid  45213  uzublem  45405  eliccelioc  45498  elicores  45510  sqrlearg  45530  fsumiunss  45552  limcdm0  45595  sumnnodd  45607  fnlimfvre  45651  limsupubuzlem  45689  limsupmnflem  45697  limsupre3uzlem  45712  climuzlem  45720  liminflelimsuplem  45752  cncfshift  45851  cncfperiod  45856  icccncfext  45864  dvnprodlem1  45923  dvnprodlem2  45924  itgsin0pilem1  45927  itgsinexplem1  45931  itgsinexp  45932  ditgeqiooicc  45937  itgsubsticclem  45952  itgioocnicc  45954  itgsbtaddcnst  45959  stoweidlem34  46011  stoweidlem41  46018  stoweidlem51  46028  wallispilem2  46043  stirlinglem11  46061  dirkercncflem2  46081  fourierdlem5  46089  fourierdlem9  46093  fourierdlem17  46101  fourierdlem18  46102  fourierdlem20  46104  fourierdlem39  46123  fourierdlem48  46131  fourierdlem49  46132  fourierdlem62  46145  fourierdlem66  46149  fourierdlem68  46151  fourierdlem72  46155  fourierdlem73  46156  fourierdlem81  46164  fourierdlem83  46166  fourierdlem85  46168  fourierdlem87  46170  fourierdlem88  46171  fourierdlem92  46175  fourierdlem95  46178  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  etransclem24  46235  etransclem35  46246  etransclem37  46248  salexct  46311  salgencntex  46320  sge0resplit  46383  sge0split  46386  meaiuninclem  46457  caratheodorylem1  46503  volicorescl  46530  hoidmv1lelem3  46570  opnvonmbllem2  46610  ovolval2  46621  ovolval3  46624  ovolval4lem1  46626  ovolval4lem2  46627  pimiooltgt  46687  sssmf  46715  smfaddlem1  46740  smflimlem2  46749  smfrec  46766  smfdiv  46774  smfsuplem1  46788  smfsuplem3  46790  et-ltneverrefl  46848  natglobalincr  46854  fcores  47044  rehalfge1  47312  spr0el  47444  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  upgrimpthslem2  47869  stgredgiun  47918  isubgr3stgrlem7  47932  fldhmsubcALTV  48256  fvconst0ci  48814  fvconstdomi  48815  idfullsubc  49048  initopropdlemlem  49104