Theorem sseli 3963

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sselii  3964  sseldi  3965  elun1  4152  elun2  4153  elopabran  5448  copsex2ga  5680  2elresin  6468  nfvres  6706  fvco4i  6762  mptrcl  6777  fvmptss  6780  fvmptex  6782  fvmptnf  6790  elfvmptrab1w  6794  elfvmptrab1  6795  fvopab4ndm  6797  fvimacnvi  6822  elpreima  6828  iinpreima  6837  ofrfval  7417  ofval  7418  off  7424  nnon  7586  finds  7608  finds2  7610  eqopi  7725  op1steq  7733  dfoprab4  7753  bropopvvv  7785  bropfvvvv  7787  reldmtpos  7900  wfrlem10  7964  smores2  7991  frsuc  8072  nnfi  8711  unifpw  8827  cantnfp1lem1  9141  cantnfp1lem3  9143  r1fin  9202  r1tr  9205  r1ordg  9207  r1ord3g  9208  r1val1  9215  tz9.12lem3  9218  tcrank  9313  cplem1  9318  hta  9326  tskwe  9379  cardprclem  9408  alephfplem3  9532  dfac12r  9572  ackbij1lem16  9657  ackbij2  9665  fin23lem28  9762  fin23lem30  9764  fin23lem31  9765  fin1a2lem6  9827  hsmexlem4  9851  hsmexlem5  9852  hsmexlem6  9853  axdc2lem  9870  axdc3lem2  9873  axcclem  9879  ac6num  9901  brdom5  9951  brdom4  9952  r1tskina  10204  gruina  10240  grur1a  10241  pinn  10300  0nnq  10346  elpqn  10347  recn  10627  rexr  10687  ltord1  11166  leord1  11167  eqord1  11168  nnre  11645  nncn  11646  nnind  11656  nnnn0  11905  nn0re  11907  nn0cn  11908  nn0xnn0  11972  nnz  12005  nn0z  12006  nnq  12362  qcn  12363  rpre  12398  eliccxr  12824  difreicc  12871  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  fzval2  12896  fzelp1  12960  4fvwrd4  13028  elfzo1  13088  ico01fl0  13190  expcllem  13441  expcl2lem  13442  m1expcl2  13452  bcm1k  13676  bcpasc  13682  hashbclem  13811  wrdv  13878  pfxfv0  14054  pfxfvlsw  14057  cshimadifsn  14191  swrds2m  14303  sqrlem5  14606  cau3lem  14714  caubnd  14718  climconst2  14905  o1of2  14969  o1rlimmul  14975  caurcvg  15033  caucvg  15035  binomlem  15184  incexclem  15191  divcnvshft  15210  zprod  15291  fprodge1  15349  risefaccllem  15367  fallfaccllem  15368  bpolydiflem  15408  bpoly4  15413  dvdsflip  15667  divalglem8  15751  sadadd  15816  smumul  15842  isprm3  16027  phimullem  16116  prmdiveq  16123  unbenlem  16244  vdwnnlem1  16331  vdwnnlem3  16333  ramtcl2  16347  prmgaplem4  16390  cshwshashlem1  16429  structcnvcnv  16497  fvsetsid  16515  imasdsval2  16789  mreunirn  16872  mrcfval  16879  mrisval  16901  coapm  17331  tsrss  17833  submnd0  17940  smndex1id  18076  nmzsubg  18317  nmznsg  18320  cntzmhm  18469  symgtrinv  18600  pmtrdifellem4  18607  psgnpmtr  18638  efginvrel2  18853  efginvrel1  18854  efgsp1  18863  efgsres  18864  efgsfo  18865  frgpinv  18890  frgpupf  18899  frgpup1  18901  subcmn  18957  torsubg  18974  dprd2dlem1  19163  dpjidcl  19180  ablfaclem3  19209  acsfn1p  19578  lssacs  19739  psrbaglefi  20152  mplsubglem  20214  ressmpladd  20238  ressmplmul  20239  ressmplvsca  20240  mplmonmul  20245  ply1bascl  20371  cnsubdrglem  20596  rege0subm  20601  rge0srg  20616  zringunit  20635  znrrg  20712  psgnghm  20724  zrhpsgnevpm  20735  evpmodpmf1o  20740  pmtrodpm  20741  phlssphl  20803  frlmsslsp  20940  islinds4  20979  lmimlbs  20980  lbslcic  20985  mdetralt  21217  mdetunilem7  21227  chfacfpmmulgsum2  21473  tgval2  21564  ordtbas  21800  ordtrestixx  21830  hauslly  22100  kgentop  22150  ptbasin  22185  filunirn  22490  uzrest  22505  elflim  22579  flffval  22597  fclsval  22616  isfcls  22617  fcfval  22641  ustn0  22829  fmucndlem  22900  xmetunirn  22947  mopnval  23048  setsmstopn  23088  tmsval  23091  tngtopn  23259  qtopbaslem  23367  xrtgioo  23414  reperflem  23426  icccmplem1  23430  icopnfhmeo  23547  icccvx  23554  bndth  23562  reparphti  23601  pcoval1  23617  pcoval2  23620  pcoass  23628  pcorevlem  23630  pcorev2  23632  pi1xfrcnv  23661  csscld  23852  cfilfval  23867  caufval  23878  bcthlem1  23927  ivthlem1  24052  ivthlem3  24054  ovolicc2lem3  24120  ovolicc2lem4  24121  vitalilem1  24209  mbflimsup  24267  i1fd  24282  i1f0  24288  i1f1  24291  itg1addlem4  24300  itg1addlem5  24301  iblmbf  24368  ellimc2  24475  limcres  24484  limcun  24493  dvbsss  24500  perfdvf  24501  dvres2lem  24508  dvaddbr  24535  rolle  24587  cmvth  24588  dvlip  24590  dvlipcn  24591  dvle  24604  lhop1lem  24610  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  ftc2  24641  itgparts  24644  itgsubstlem  24645  itgsubst  24646  deg1mul3  24709  coeval  24813  coeeu  24815  dgrval  24818  coef3  24822  coemulc  24845  dgrsub  24862  coecj  24868  dvply2  24875  dvnply  24877  quotval  24881  fta1  24897  plyexmo  24902  aacjcl  24916  taylfval  24947  dvtaylp  24958  abelth  25029  pilem3  25041  sinord  25118  recosf1o  25119  resinf1o  25120  tanord1  25121  eff1olem  25132  dvloglem  25231  dvlog  25234  dvlog2lem  25235  advlogexp  25238  logtayl  25243  logtayl2  25245  dvcncxp1  25324  dvcnsqrt  25325  cxpcn3lem  25328  cxpcn3  25329  sqrtcn  25331  loglesqrt  25339  1cubr  25420  acosrecl  25481  efrlim  25547  jensen  25566  lgamgulmlem2  25607  lgamucov2  25616  basellem4  25661  musum  25768  dchrinvcl  25829  dchrghm  25832  dchrinv  25837  dchrsum2  25844  dchrsum  25845  rpvmasumlem  26063  dchrisum0lem2a  26093  pnt  26190  tglng  26332  axlowdimlem6  26733  axlowdimlem16  26743  axlowdimlem17  26744  axlowdim  26747  axeuclidlem  26748  axcontlem2  26751  axcontlem7  26756  axcontlem8  26757  nbusgrvtxm1uvtx  27187  wlk1walk  27420  pthdivtx  27510  pthdadjvtx  27511  crctcshwlkn0lem2  27589  crctcshwlkn0lem4  27591  clwwisshclwws  27793  fusgreg2wsp  28115  nvvcop  28371  nvex  28388  phnv  28591  sheli  28991  cheli  29009  hhssabloilem  29038  choc1  29104  shintcli  29106  chintcli  29108  shsleji  29147  pjini  29476  mayete3i  29505  dmadjop  29665  nlelshi  29837  cnlnadjeui  29854  cnlnssadj  29857  bdopadj  29859  pjimai  29953  stcl  29993  atelch  30121  fcnvgreu  30418  f1od2  30457  fcobijfs  30459  uzssico  30507  iundisj2fi  30520  nnindf  30535  eliccioo  30607  gsummptres  30690  cyc3genpm  30794  ordtrestNEW  31164  xrge0iifcnv  31176  xrge0iifcv  31177  xrge0iifiso  31178  xrge0iifhom  31180  qqhcn  31232  esumval  31305  gsumesum  31318  esumlub  31319  esumcst  31322  esumfsup  31329  issgon  31382  elrnsiga  31385  imambfm  31520  br2base  31527  sxbrsigalem0  31529  dya2iocucvr  31542  sxbrsigalem2  31544  sxbrsigalem5  31546  sxbrsiga  31548  omssubadd  31558  sitmcl  31609  oddpwdc  31612  eulerpartlemelr  31615  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgs2  31638  eulerpartlemn  31639  sseqf  31650  ballotlem2  31746  ballotlemfp1  31749  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemfmpn  31752  ballotlemsup  31762  ballotlemfrceq  31786  signswch  31831  rpsqrtcn  31864  prodfzo03  31874  itgexpif  31877  bnj1533  32124  bnj1137  32267  bnj1286  32291  bnj1408  32308  bnj1417  32313  subfacp1lem5  32431  cvmsi  32512  gonar  32642  goalr  32644  mpst123  32787  mpstrcl  32788  msrrcl  32790  elmsta  32795  msubvrs  32807  elmpps  32820  elmthm  32823  bcprod  32970  dfon2lem4  33031  pprodss4v  33345  ivthALT  33683  neibastop2lem  33708  nnssi2  33803  nnssi3  33804  bj-sngltagi  34297  bj-elid5  34464  bj-fvmptunsn1  34542  bj-smgrpssmgmel  34554  bj-mndsssmgrpel  34556  bj-cmnssmndel  34558  bj-grpssmndel  34560  bj-ablssgrpel  34562  bj-ablsscmnel  34564  bj-vecssmodel  34567  bj-rveccvec  34589  bj-rvecabl  34591  taupilemrplb  34604  icorempo  34635  elxp8  34655  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem14  34921  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  poimirlem32  34939  mblfinlem1  34944  cnambfre  34955  dvtan  34957  itg2addnc  34961  itg2gt0cn  34962  ftc1cnnc  34981  ftc2nc  34991  dvasin  34993  dvacos  34994  cover2  35004  sstotbnd2  35067  heibor1lem  35102  heiborlem10  35113  opidonOLD  35145  exidcl  35169  rngosn3  35217  flddivrng  35292  toycom  36124  osumcllem7N  37113  pexmidlem4N  37124  diaintclN  38209  dibintclN  38318  mapd1o  38799  hdmapevec  38986  prjspvs  39309  prjspeclsp  39311  0prjspnrel  39318  elrfi  39340  elrfirn  39341  elrfirn2  39342  mrefg3  39354  diophin  39418  diophun  39419  eq0rabdioph  39422  eqrabdioph  39423  pellex  39481  rmxycomplete  39563  jm2.23  39642  aomclem2  39704  fglmod  39722  lsmfgcl  39723  lmhmfgima  39733  lmhmfgsplit  39735  isnumbasabl  39755  dgrsub2  39784  itgocn  39813  areaquad  39872  elmapintrab  39985  corcltrcl  40133  k0004val0  40553  elscottab  40629  radcnvrat  40695  uzmptshftfval  40727  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  onfrALTlem2  40929  onfrALTlem2VD  41272  uzwo4  41364  disjinfi  41503  mptssid  41560  uzublem  41753  eliccelioc  41846  elicores  41858  sqrlearg  41878  fsumiunss  41905  limcdm0  41948  sumnnodd  41960  fnlimfvre  42004  limsupubuzlem  42042  limsupmnflem  42050  limsupre3uzlem  42065  climuzlem  42073  cncfshift  42206  cncfperiod  42211  icccncfext  42219  dvnprodlem1  42280  dvnprodlem2  42281  itgsin0pilem1  42284  itgsinexplem1  42288  itgsinexp  42289  ditgeqiooicc  42294  itgsubsticclem  42309  itgioocnicc  42311  itgsbtaddcnst  42316  stoweidlem34  42368  stoweidlem41  42375  stoweidlem51  42385  wallispilem2  42400  stirlinglem11  42418  dirkercncflem2  42438  fourierdlem5  42446  fourierdlem9  42450  fourierdlem17  42458  fourierdlem18  42459  fourierdlem20  42461  fourierdlem39  42480  fourierdlem48  42488  fourierdlem49  42489  fourierdlem62  42502  fourierdlem66  42506  fourierdlem68  42508  fourierdlem72  42512  fourierdlem73  42513  fourierdlem81  42521  fourierdlem83  42523  fourierdlem85  42525  fourierdlem87  42527  fourierdlem88  42528  fourierdlem92  42532  fourierdlem95  42535  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  etransclem24  42592  etransclem35  42603  etransclem37  42605  salexct  42666  salgencntex  42675  sge0resplit  42737  sge0split  42740  meaiuninclem  42811  caratheodorylem1  42857  volicorescl  42884  hoidmv1lelem3  42924  opnvonmbllem2  42964  ovolval2  42975  ovolval3  42978  ovolval4lem1  42980  ovolval4lem2  42981  pimiooltgt  43038  sssmf  43064  smfaddlem1  43088  smflimlem2  43097  smfrec  43113  smfdiv  43121  smfsuplem1  43134  smfsuplem3  43136  spr0el  43693  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  fldhmsubc  44404  fldhmsubcALTV  44422  setrec2lem1  44845