Theorem sseli 4004

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  sselii  4005  sselid  4006  elun1  4205  elun2  4206  elopabr  5580  elopabran  5581  elopaelxp  5789  copsex2ga  5831  2elresin  6701  nfvres  6961  fvco4i  7023  mptrcl  7038  fvmptss  7041  fvmptex  7043  fvmptnf  7051  elfvmptrab1w  7056  elfvmptrab1  7057  fvopab4ndm  7059  fvimacnvi  7085  elpreima  7091  iinpreima  7102  ofrfvalg  7722  ofval  7725  off  7732  nnon  7909  finds  7936  finds2  7938  eqopi  8066  op1steq  8074  dfoprab4  8096  bropopvvv  8131  bropfvvvv  8133  reldmtpos  8275  wfrlem10OLD  8374  smores2  8410  frsuc  8493  nnfiOLD  9295  unifpw  9425  cantnfp1lem1  9747  cantnfp1lem3  9749  r1fin  9842  r1tr  9845  r1ordg  9847  r1ord3g  9848  r1val1  9855  tz9.12lem3  9858  tcrank  9953  cplem1  9958  hta  9966  tskwe  10019  cardprclem  10048  alephfplem3  10175  dfac12r  10216  ackbij1lem16  10303  ackbij2  10311  fin23lem28  10409  fin23lem30  10411  fin23lem31  10412  fin1a2lem6  10474  hsmexlem4  10498  hsmexlem5  10499  hsmexlem6  10500  axdc2lem  10517  axdc3lem2  10520  axcclem  10526  brdom5  10598  brdom4  10599  r1tskina  10851  gruina  10887  grur1a  10888  pinn  10947  0nnq  10993  elpqn  10994  recn  11274  rexr  11336  ltord1  11816  leord1  11817  eqord1  11818  nnre  12300  nncn  12301  nnind  12311  nnnn0  12560  nn0re  12562  nn0cn  12563  nn0xnn0  12629  nnzOLD  12663  nn0z  12664  nnq  13027  qcn  13028  rpre  13065  eliccxr  13495  difreicc  13544  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  fzval2  13570  fzelp1  13636  4fvwrd4  13705  elfzo1  13766  ico01fl0  13870  expcllem  14123  expcl2lem  14124  m1expcl2  14136  bcm1k  14364  bcpasc  14370  hashbclem  14501  wrdv  14577  pfxfv0  14740  pfxfvlsw  14743  cshimadifsn  14878  swrds2m  14990  01sqrexlem5  15295  cau3lem  15403  caubnd  15407  climconst2  15594  o1of2  15659  o1rlimmul  15665  caurcvg  15725  caucvg  15727  binomlem  15877  incexclem  15884  divcnvshft  15903  zprod  15985  fprodge1  16043  risefaccllem  16061  fallfaccllem  16062  bpolydiflem  16102  bpoly4  16107  dvdsflip  16365  divalglem8  16448  sadadd  16513  smumul  16539  isprm3  16730  phimullem  16826  prmdiveq  16833  unbenlem  16955  vdwnnlem1  17042  vdwnnlem3  17044  ramtcl2  17058  prmgaplem4  17101  cshwshashlem1  17143  structcnvcnv  17200  fvsetsid  17215  imasdsval2  17576  mreunirn  17659  mrcfval  17666  mrisval  17688  coapm  18138  tsrss  18659  submnd0  18801  smndex1id  18946  nmzsubg  19205  nmznsg  19208  cntzmhm  19381  symgtrinv  19514  pmtrdifellem4  19521  psgnpmtr  19552  efginvrel2  19769  efginvrel1  19770  efgsp1  19779  efgsres  19780  efgsfo  19781  frgpinv  19806  frgpupf  19815  frgpup1  19817  subcmn  19879  torsubg  19896  dprd2dlem1  20085  dpjidcl  20102  ablfaclem3  20131  nzrring  20542  lringnzr  20567  fldhmsubc  20808  acsfn1p  20822  lssacs  20988  cnsubdrglem  21459  rege0subm  21464  rge0srg  21479  zringunit  21500  znrrg  21607  psgnghm  21621  zrhpsgnevpm  21632  evpmodpmf1o  21637  pmtrodpm  21638  phlssphl  21700  frlmsslsp  21839  islinds4  21878  lmimlbs  21879  lbslcic  21884  psrbaglefi  21969  psrbagconf1o  21972  mplsubglem  22042  mplneg  22053  ressmpladd  22070  ressmplmul  22071  ressmplvsca  22072  mplmonmul  22077  psdmul  22193  ply1bascl  22226  mdetralt  22635  mdetunilem7  22645  chfacfpmmulgsum2  22892  tgval2  22984  ordtbas  23221  ordtrestixx  23251  hauslly  23521  kgentop  23571  ptbasin  23606  filunirn  23911  uzrest  23926  elflim  24000  flffval  24018  fclsval  24037  isfcls  24038  fcfval  24062  ustn0  24250  fmucndlem  24321  xmetunirn  24368  mopnval  24469  setsmstopn  24511  tmsval  24514  tngtopn  24692  qtopbaslem  24800  xrtgioo  24847  reperflem  24859  icccmplem1  24863  icopnfhmeo  24993  icccvx  25000  bndth  25009  reparphtiOLD  25049  pcoval1  25065  pcoval2  25068  pcoass  25076  pcorevlem  25078  pcorev2  25080  pi1xfrcnv  25109  csscld  25302  cfilfval  25317  caufval  25328  bcthlem1  25377  ivthlem1  25505  ivthlem3  25507  ovolicc2lem3  25573  ovolicc2lem4  25574  vitalilem1  25662  mbflimsup  25720  i1fd  25735  i1f0  25741  i1f1  25744  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  iblmbf  25822  ellimc2  25932  limcres  25941  limcun  25950  dvbsss  25957  perfdvf  25958  dvres2lem  25965  dvaddbr  25994  rolle  26048  cmvth  26049  cmvthOLD  26050  dvlip  26052  dvlipcn  26053  dvle  26066  lhop1lem  26072  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc2  26105  itgparts  26108  itgsubstlem  26109  itgsubst  26110  deg1mul3  26175  coeval  26282  coeeu  26284  dgrval  26287  coef3  26291  coemulc  26314  dgrsub  26332  coecj  26338  dvply2  26346  dvnply  26348  quotval  26352  fta1  26368  plyexmo  26373  aacjcl  26387  taylfval  26418  dvtaylp  26430  abelth  26503  pilem3  26515  cos0pilt1  26592  sinord  26594  recosf1o  26595  resinf1o  26596  tanord1  26597  eff1olem  26608  dvloglem  26708  dvlog  26711  dvlog2lem  26712  advlogexp  26715  logtayl  26720  logtayl2  26722  dvcncxp1  26803  dvcnsqrt  26804  cxpcn3lem  26808  cxpcn3  26809  sqrtcn  26811  loglesqrt  26822  1cubr  26903  acosrecl  26964  efrlim  27030  efrlimOLD  27031  jensen  27050  lgamgulmlem2  27091  lgamucov2  27100  basellem4  27145  musum  27252  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dchrinvcl  27315  dchrghm  27318  dchrinv  27323  dchrsum2  27330  dchrsum  27331  rpvmasumlem  27549  dchrisum0lem2a  27579  pnt  27676  oldf  27914  leftirr  27947  rightirr  27948  lrold  27953  sltlpss  27963  addsproplem2  28021  sleadd1  28040  addsuniflem  28052  addsbdaylem  28067  addsbday  28068  negsproplem2  28079  negsid  28091  negsunif  28105  mulsrid  28157  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  precsexlem9  28257  precsexlem11  28259  onsno  28296  onaddscl  28304  onmulscl  28305  n0sno  28346  nnsno  28347  nnn0s  28350  nnsgt0  28360  zno  28386  tglng  28572  axlowdimlem6  28980  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  axeuclidlem  28995  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  nbusgrvtxm1uvtx  29440  wlk1walk  29675  pthdivtx  29765  pthdadjvtx  29766  crctcshwlkn0lem2  29844  crctcshwlkn0lem4  29846  clwwisshclwws  30047  fusgreg2wsp  30368  nvvcop  30626  nvex  30643  phnv  30846  sheli  31246  cheli  31264  hhssabloilem  31293  choc1  31359  shintcli  31361  chintcli  31363  shsleji  31402  pjini  31731  mayete3i  31760  dmadjop  31920  nlelshi  32092  cnlnadjeui  32109  cnlnssadj  32112  bdopadj  32114  pjimai  32208  stcl  32248  atelch  32376  fcnvgreu  32691  f1od2  32735  fcobijfs  32737  uzssico  32789  iundisj2fi  32802  nnindf  32823  eliccioo  32895  gsummptres  33035  cyc3genpm  33145  elrspunidl  33421  zarcls  33820  ordtrestNEW  33867  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  qqhcn  33937  esumval  34010  gsumesum  34023  esumlub  34024  esumcst  34027  esumfsup  34034  issgon  34087  elrnsiga  34090  imambfm  34227  br2base  34234  sxbrsigalem0  34236  dya2iocucvr  34249  sxbrsigalem2  34251  sxbrsigalem5  34253  sxbrsiga  34255  omssubadd  34265  sitmcl  34316  oddpwdc  34319  eulerpartlemelr  34322  eulerpartlemgvv  34341  eulerpartlemgh  34343  eulerpartlemgs2  34345  eulerpartlemn  34346  sseqf  34357  ballotlem2  34453  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfmpn  34459  ballotlemsup  34469  ballotlemfrceq  34493  signswch  34538  rpsqrtcn  34570  prodfzo03  34580  itgexpif  34583  bnj1533  34828  bnj1137  34971  bnj1286  34995  bnj1408  35012  bnj1417  35017  subfacp1lem5  35152  cvmsi  35233  gonar  35363  goalr  35365  mpst123  35508  mpstrcl  35509  msrrcl  35511  elmsta  35516  msubvrs  35528  elmpps  35541  elmthm  35544  bcprod  35700  dfon2lem4  35750  pprodss4v  35848  ivthALT  36301  neibastop2lem  36326  nnssi2  36421  nnssi3  36422  bj-sngltagi  36948  bj-elid5  37135  bj-fvmptunsn1  37223  bj-smgrpssmgmel  37235  bj-mndsssmgrpel  37237  bj-cmnssmndel  37239  bj-grpssmndel  37241  bj-ablssgrpel  37243  bj-ablsscmnel  37245  bj-vecssmodel  37248  bj-flddrng  37255  bj-rveccvec  37271  bj-rvecabl  37273  taupilemrplb  37286  icorempo  37317  elxp8  37337  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem14  37594  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  mblfinlem1  37617  cnambfre  37628  dvtan  37630  itg2addnc  37634  itg2gt0cn  37635  ftc1cnnc  37652  ftc2nc  37662  dvasin  37664  dvacos  37665  cover2  37675  sstotbnd2  37734  heibor1lem  37769  heiborlem10  37780  opidonOLD  37812  exidcl  37836  rngosn3  37884  flddivrng  37959  toycom  38929  osumcllem7N  39919  pexmidlem4N  39930  diaintclN  41015  dibintclN  41124  mapd1o  41605  hdmapevec  41792  dvrelog2  42021  aks6d1c2lem4  42084  sticksstones1  42103  aks6d1c6lem5  42134  imacrhmcl  42469  prjspvs  42565  prjspeclsp  42567  0prjspnrel  42582  elrfi  42650  elrfirn  42651  elrfirn2  42652  mrefg3  42664  diophin  42728  diophun  42729  eq0rabdioph  42732  eqrabdioph  42733  pellex  42791  rmxycomplete  42874  jm2.23  42953  aomclem2  43012  fglmod  43030  lsmfgcl  43031  lmhmfgima  43041  lmhmfgsplit  43043  isnumbasabl  43063  dgrsub2  43092  itgocn  43121  areaquad  43177  cantnftermord  43282  omabs2  43294  nna1iscard  43507  elmapintrab  43538  corcltrcl  43701  k0004val0  44116  elscottab  44213  radcnvrat  44283  uzmptshftfval  44315  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  onfrALTlem2  44517  onfrALTlem2VD  44860  uzwo4  44955  mptssid  45149  uzublem  45345  eliccelioc  45439  elicores  45451  sqrlearg  45471  fsumiunss  45496  limcdm0  45539  sumnnodd  45551  fnlimfvre  45595  limsupubuzlem  45633  limsupmnflem  45641  limsupre3uzlem  45656  climuzlem  45664  cncfshift  45795  cncfperiod  45800  icccncfext  45808  dvnprodlem1  45867  dvnprodlem2  45868  itgsin0pilem1  45871  itgsinexplem1  45875  itgsinexp  45876  ditgeqiooicc  45881  itgsubsticclem  45896  itgioocnicc  45898  itgsbtaddcnst  45903  stoweidlem34  45955  stoweidlem41  45962  stoweidlem51  45972  wallispilem2  45987  stirlinglem11  46005  dirkercncflem2  46025  fourierdlem5  46033  fourierdlem9  46037  fourierdlem17  46045  fourierdlem18  46046  fourierdlem20  46048  fourierdlem39  46067  fourierdlem48  46075  fourierdlem49  46076  fourierdlem62  46089  fourierdlem66  46093  fourierdlem68  46095  fourierdlem72  46099  fourierdlem73  46100  fourierdlem81  46108  fourierdlem83  46110  fourierdlem85  46112  fourierdlem87  46114  fourierdlem88  46115  fourierdlem92  46119  fourierdlem95  46122  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  etransclem24  46179  etransclem35  46190  etransclem37  46192  salexct  46255  salgencntex  46264  sge0resplit  46327  sge0split  46330  meaiuninclem  46401  caratheodorylem1  46447  volicorescl  46474  hoidmv1lelem3  46514  opnvonmbllem2  46554  ovolval2  46565  ovolval3  46568  ovolval4lem1  46570  ovolval4lem2  46571  pimiooltgt  46631  sssmf  46659  smfaddlem1  46684  smflimlem2  46693  smfrec  46710  smfdiv  46718  smfsuplem1  46732  smfsuplem3  46734  et-ltneverrefl  46792  natglobalincr  46796  fcores  46982  spr0el  47356  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  fldhmsubcALTV  48056  fvconst0ci  48572  fvconstdomi  48573