Theorem sseli 3939

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

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

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 3928

This theorem is referenced by:  sselii  3940  sselid  3941  elun1  4141  elun2  4142  elopabr  5515  elopabran  5516  elopaelxp  5721  copsex2ga  5761  2elresin  6621  nfvres  6881  fvco4i  6944  mptrcl  6959  fvmptss  6962  fvmptex  6964  fvmptnf  6972  elfvmptrab1w  6977  elfvmptrab1  6978  fvopab4ndm  6980  fvimacnvi  7006  elpreima  7012  iinpreima  7023  ofrfvalg  7641  ofval  7644  off  7651  nnon  7828  finds  7852  finds2  7854  eqopi  7983  op1steq  7991  dfoprab4  8013  bropopvvv  8046  bropfvvvv  8048  reldmtpos  8190  smores2  8300  frsuc  8382  unifpw  9282  cantnfp1lem1  9607  cantnfp1lem3  9609  r1fin  9702  r1tr  9705  r1ordg  9707  r1ord3g  9708  r1val1  9715  tz9.12lem3  9718  tcrank  9813  cplem1  9818  hta  9826  tskwe  9879  cardprclem  9908  alephfplem3  10035  dfac12r  10076  ackbij1lem16  10163  ackbij2  10171  fin23lem28  10269  fin23lem30  10271  fin23lem31  10272  fin1a2lem6  10334  hsmexlem4  10358  hsmexlem5  10359  hsmexlem6  10360  axdc2lem  10377  axdc3lem2  10380  axcclem  10386  brdom5  10458  brdom4  10459  r1tskina  10711  gruina  10747  grur1a  10748  pinn  10807  0nnq  10853  elpqn  10854  recn  11134  rexr  11196  ltord1  11680  leord1  11681  eqord1  11682  nnre  12169  nncn  12170  nnind  12180  nnnn0  12425  nn0re  12427  nn0cn  12428  nn0xnn0  12495  nnzOLD  12529  nn0z  12530  uzuzle35  12822  nnq  12897  qcn  12898  rpre  12936  eliccxr  13372  difreicc  13421  iccshftri  13424  iccshftli  13426  iccdili  13428  icccntri  13430  fzval2  13447  fzelp1  13513  4fvwrd4  13585  elfzo1  13649  ico01fl0  13757  expcllem  14013  expcl2lem  14014  m1expcl2  14026  bcm1k  14256  bcpasc  14262  hashbclem  14393  wrdv  14470  pfxfv0  14633  pfxfvlsw  14636  cshimadifsn  14771  swrds2m  14883  01sqrexlem5  15188  cau3lem  15297  caubnd  15301  climconst2  15490  o1of2  15555  o1rlimmul  15561  caurcvg  15619  caucvg  15621  binomlem  15771  incexclem  15778  divcnvshft  15797  zprod  15879  fprodge1  15937  risefaccllem  15955  fallfaccllem  15956  bpolydiflem  15996  bpoly4  16001  dvdsflip  16263  divalglem8  16346  sadadd  16413  smumul  16439  isprm3  16629  phimullem  16725  prmdiveq  16732  unbenlem  16855  vdwnnlem1  16942  vdwnnlem3  16944  ramtcl2  16958  prmgaplem4  17001  cshwshashlem1  17042  structcnvcnv  17099  fvsetsid  17114  imasdsval2  17455  mreunirn  17538  mrcfval  17545  mrisval  17567  coapm  18009  tsrss  18524  submnd0  18666  smndex1id  18814  nmzsubg  19073  nmznsg  19076  cntzmhm  19249  symgtrinv  19378  pmtrdifellem4  19385  psgnpmtr  19416  efginvrel2  19633  efginvrel1  19634  efgsp1  19643  efgsres  19644  efgsfo  19645  frgpinv  19670  frgpupf  19679  frgpup1  19681  subcmn  19743  torsubg  19760  dprd2dlem1  19949  dpjidcl  19966  ablfaclem3  19995  nzrring  20401  lringnzr  20426  fldhmsubc  20670  acsfn1p  20684  lssacs  20849  cnsubdrglem  21311  rege0subm  21316  rge0srg  21331  zringunit  21352  znrrg  21451  psgnghm  21465  zrhpsgnevpm  21476  evpmodpmf1o  21481  pmtrodpm  21482  phlssphl  21544  frlmsslsp  21681  islinds4  21720  lmimlbs  21721  lbslcic  21726  psrbaglefi  21811  psrbagconf1o  21814  mplsubglem  21884  mplneg  21895  ressmpladd  21912  ressmplmul  21913  ressmplvsca  21914  mplmonmul  21919  psdmul  22029  ply1bascl  22064  mdetralt  22471  mdetunilem7  22481  chfacfpmmulgsum2  22728  tgval2  22819  ordtbas  23055  ordtrestixx  23085  hauslly  23355  kgentop  23405  ptbasin  23440  filunirn  23745  uzrest  23760  elflim  23834  flffval  23852  fclsval  23871  isfcls  23872  fcfval  23896  ustn0  24084  fmucndlem  24154  xmetunirn  24201  mopnval  24302  setsmstopn  24342  tmsval  24345  tngtopn  24514  qtopbaslem  24622  xrtgioo  24671  reperflem  24683  icccmplem1  24687  icopnfhmeo  24817  icccvx  24824  bndth  24833  reparphtiOLD  24873  pcoval1  24889  pcoval2  24892  pcoass  24900  pcorevlem  24902  pcorev2  24904  pi1xfrcnv  24933  csscld  25125  cfilfval  25140  caufval  25151  bcthlem1  25200  ivthlem1  25328  ivthlem3  25330  ovolicc2lem3  25396  ovolicc2lem4  25397  vitalilem1  25485  mbflimsup  25543  i1fd  25558  i1f0  25564  i1f1  25567  itg1addlem4  25576  itg1addlem5  25577  iblmbf  25644  ellimc2  25754  limcres  25763  limcun  25772  dvbsss  25779  perfdvf  25780  dvres2lem  25787  dvaddbr  25816  rolle  25870  cmvth  25871  cmvthOLD  25872  dvlip  25874  dvlipcn  25875  dvle  25888  lhop1lem  25894  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  ftc2  25927  itgparts  25930  itgsubstlem  25931  itgsubst  25932  deg1mul3  25997  coeval  26104  coeeu  26106  dgrval  26109  coef3  26113  coemulc  26136  dgrsub  26154  coecj  26160  coecjOLD  26162  dvply2  26170  dvnply  26172  quotval  26176  fta1  26192  plyexmo  26197  aacjcl  26211  taylfval  26242  dvtaylp  26254  abelth  26327  pilem3  26339  cos0pilt1  26417  sinord  26419  recosf1o  26420  resinf1o  26421  tanord1  26422  eff1olem  26433  dvloglem  26533  dvlog  26536  dvlog2lem  26537  advlogexp  26540  logtayl  26545  logtayl2  26547  dvcncxp1  26628  dvcnsqrt  26629  cxpcn3lem  26633  cxpcn3  26634  sqrtcn  26636  loglesqrt  26647  1cubr  26728  acosrecl  26789  efrlim  26855  efrlimOLD  26856  jensen  26875  lgamgulmlem2  26916  lgamucov2  26925  basellem4  26970  musum  27077  mpodvdsmulf1o  27080  fsumdvdsmul  27081  dchrinvcl  27140  dchrghm  27143  dchrinv  27148  dchrsum2  27155  dchrsum  27156  rpvmasumlem  27374  dchrisum0lem2a  27404  pnt  27501  oldf  27741  leftirr  27778  rightirr  27779  lrold  27784  newbdayim  27790  sltlpss  27795  addsproplem2  27853  sleadd1  27872  addsuniflem  27884  addsbdaylem  27899  addsbday  27900  negsproplem2  27911  negsid  27923  negsunif  27937  mulsrid  27992  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  precsexlem9  28093  precsexlem11  28095  onsno  28132  onscutlt  28141  onaddscl  28150  onmulscl  28151  n0sno  28192  nnsno  28193  nnn0s  28196  nnsgt0  28207  zno  28246  expscllem  28292  tglng  28449  axlowdimlem6  28850  axlowdimlem16  28860  axlowdimlem17  28861  axlowdim  28864  axeuclidlem  28865  axcontlem2  28868  axcontlem7  28873  axcontlem8  28874  nbusgrvtxm1uvtx  29308  wlk1walk  29542  pthdivtx  29630  pthdadjvtx  29631  crctcshwlkn0lem2  29714  crctcshwlkn0lem4  29716  clwwisshclwws  29917  fusgreg2wsp  30238  nvvcop  30496  nvex  30513  phnv  30716  sheli  31116  cheli  31134  hhssabloilem  31163  choc1  31229  shintcli  31231  chintcli  31233  shsleji  31272  pjini  31601  mayete3i  31630  dmadjop  31790  nlelshi  31962  cnlnadjeui  31979  cnlnssadj  31982  bdopadj  31984  pjimai  32078  stcl  32118  atelch  32246  fcnvgreu  32570  f1od2  32617  fcobijfs  32619  uzssico  32680  iundisj2fi  32693  nnindf  32717  eliccioo  32824  gsummptres  32965  cyc3genpm  33082  elrspunidl  33372  zarcls  33837  ordtrestNEW  33884  xrge0iifcnv  33896  xrge0iifcv  33897  xrge0iifiso  33898  xrge0iifhom  33900  qqhcn  33954  esumval  34009  gsumesum  34022  esumlub  34023  esumcst  34026  esumfsup  34033  issgon  34086  elrnsiga  34089  imambfm  34226  br2base  34233  sxbrsigalem0  34235  dya2iocucvr  34248  sxbrsigalem2  34250  sxbrsigalem5  34252  sxbrsiga  34254  omssubadd  34264  sitmcl  34315  oddpwdc  34318  eulerpartlemelr  34321  eulerpartlemgvv  34340  eulerpartlemgh  34342  eulerpartlemgs2  34344  eulerpartlemn  34345  sseqf  34356  ballotlem2  34453  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfmpn  34459  ballotlemsup  34469  ballotlemfrceq  34493  signswch  34525  rpsqrtcn  34557  prodfzo03  34567  itgexpif  34570  bnj1533  34815  bnj1137  34958  bnj1286  34982  bnj1408  34999  bnj1417  35004  onvf1odlem4  35066  subfacp1lem5  35144  cvmsi  35225  gonar  35355  goalr  35357  mpst123  35500  mpstrcl  35501  msrrcl  35503  elmsta  35508  msubvrs  35520  elmpps  35533  elmthm  35536  bcprod  35698  dfon2lem4  35747  pprodss4v  35845  ivthALT  36296  neibastop2lem  36321  nnssi2  36416  nnssi3  36417  bj-sngltagi  36943  bj-elid5  37130  bj-fvmptunsn1  37218  bj-smgrpssmgmel  37230  bj-mndsssmgrpel  37232  bj-cmnssmndel  37234  bj-grpssmndel  37236  bj-ablssgrpel  37238  bj-ablsscmnel  37240  bj-vecssmodel  37243  bj-flddrng  37250  bj-rveccvec  37266  bj-rvecabl  37268  taupilemrplb  37281  icorempo  37312  elxp8  37332  sin2h  37577  cos2h  37578  tan2h  37579  poimirlem14  37601  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  mblfinlem1  37624  cnambfre  37635  dvtan  37637  itg2addnc  37641  itg2gt0cn  37642  ftc1cnnc  37659  ftc2nc  37669  dvasin  37671  dvacos  37672  cover2  37682  sstotbnd2  37741  heibor1lem  37776  heiborlem10  37787  opidonOLD  37819  exidcl  37843  rngosn3  37891  flddivrng  37966  toycom  38939  osumcllem7N  39929  pexmidlem4N  39940  diaintclN  41025  dibintclN  41134  mapd1o  41615  hdmapevec  41802  dvrelog2  42025  aks6d1c2lem4  42088  sticksstones1  42107  aks6d1c6lem5  42138  redvmptabs  42321  imacrhmcl  42475  prjspvs  42571  prjspeclsp  42573  0prjspnrel  42588  elrfi  42655  elrfirn  42656  elrfirn2  42657  mrefg3  42669  diophin  42733  diophun  42734  eq0rabdioph  42737  eqrabdioph  42738  pellex  42796  rmxycomplete  42879  jm2.23  42958  aomclem2  43017  fglmod  43035  lsmfgcl  43036  lmhmfgima  43046  lmhmfgsplit  43048  isnumbasabl  43068  dgrsub2  43097  itgocn  43126  areaquad  43178  cantnftermord  43282  omabs2  43294  nna1iscard  43507  elmapintrab  43538  corcltrcl  43701  k0004val0  44116  elscottab  44206  radcnvrat  44276  uzmptshftfval  44308  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  onfrALTlem2  44509  onfrALTlem2VD  44851  uzwo4  45020  mptssid  45208  uzublem  45399  eliccelioc  45492  elicores  45504  sqrlearg  45524  fsumiunss  45546  limcdm0  45589  sumnnodd  45601  fnlimfvre  45645  limsupubuzlem  45683  limsupmnflem  45691  limsupre3uzlem  45706  climuzlem  45714  liminflelimsuplem  45746  cncfshift  45845  cncfperiod  45850  icccncfext  45858  dvnprodlem1  45917  dvnprodlem2  45918  itgsin0pilem1  45921  itgsinexplem1  45925  itgsinexp  45926  ditgeqiooicc  45931  itgsubsticclem  45946  itgioocnicc  45948  itgsbtaddcnst  45953  stoweidlem34  46005  stoweidlem41  46012  stoweidlem51  46022  wallispilem2  46037  stirlinglem11  46055  dirkercncflem2  46075  fourierdlem5  46083  fourierdlem9  46087  fourierdlem17  46095  fourierdlem18  46096  fourierdlem20  46098  fourierdlem39  46117  fourierdlem48  46125  fourierdlem49  46126  fourierdlem62  46139  fourierdlem66  46143  fourierdlem68  46145  fourierdlem72  46149  fourierdlem73  46150  fourierdlem81  46158  fourierdlem83  46160  fourierdlem85  46162  fourierdlem87  46164  fourierdlem88  46165  fourierdlem92  46169  fourierdlem95  46172  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  etransclem24  46229  etransclem35  46240  etransclem37  46242  salexct  46305  salgencntex  46314  sge0resplit  46377  sge0split  46380  meaiuninclem  46451  caratheodorylem1  46497  volicorescl  46524  hoidmv1lelem3  46564  opnvonmbllem2  46604  ovolval2  46615  ovolval3  46618  ovolval4lem1  46620  ovolval4lem2  46621  pimiooltgt  46681  sssmf  46709  smfaddlem1  46734  smflimlem2  46743  smfrec  46760  smfdiv  46768  smfsuplem1  46782  smfsuplem3  46784  et-ltneverrefl  46842  natglobalincr  46848  tannpoly  46864  fcores  47041  rehalfge1  47309  spr0el  47456  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbnd  47783  upgrimpthslem2  47881  stgredgiun  47930  isubgr3stgrlem7  47944  fldhmsubcALTV  48294  fvconst0ci  48852  fvconstdomi  48853  idfullsubc  49123  fulloppf  49125  fthoppf  49126  initopropdlemlem  49201