Theorem ssexi 5262

Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
ssexi.1	⊢ 𝐵 ∈ V
ssexi.2	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
ssexi	⊢ 𝐴 ∈ V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssexi.1	. . 3 ⊢ 𝐵 ∈ V
3	2	ssex 5261	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  abex  5266  zfausab  5272  ord3ex  5328  epse  5610  opabex  7172  opabresex2  7418  mptexw  7903  fvclex  7909  oprabex  7926  mpoexw  8028  tfrlem16  8329  fosetex  8802  f1osetex  8803  dffi3  9341  r0weon  9931  dfac3  10040  dfac5lem4  10045  dfac5lem4OLD  10047  dfac2b  10050  hsmexlem6  10350  domtriomlem  10361  axdc3lem  10369  ac6  10399  brdom7disj  10450  brdom6disj  10451  niex  10801  enqex  10842  npex  10906  nrex1  10984  enrex  10987  reex  11126  nnex  12177  zex  12530  qex  12908  ixxex  13306  ltweuz  13920  seqexw  13976  cshwsexa  14783  prmex  16643  prdsval  17415  prdsle  17422  xrsle  17565  sectfval  17715  sscpwex  17779  issubc  17799  isfunc  17828  fullfunc  17872  fthfunc  17873  isfull  17876  isfth  17880  ipoval  18493  letsr  18556  ressmulgnn  19049  nmznsg  19140  eqgfval  19148  isghm  19187  isghmOLD  19188  lpival  21320  znle  21532  cssval  21678  pjfval  21702  ltbval  22037  opsrle  22041  istopon  22893  dmtopon  22904  leordtval2  23193  lecldbas  23200  xkoopn  23570  xkouni  23580  xkoccn  23600  xkoco1cn  23638  xkoco2cn  23639  xkococn  23641  xkoinjcn  23668  uzrest  23878  ustfn  24183  ustn0  24202  isphtpc  24977  tcphex  25200  tchnmfval  25211  bcthlem1  25307  bcthlem5  25311  dyadmbl  25583  itg2seq  25725  aannenlem3  26313  psercn  26410  abelth  26425  vmadivsum  27465  rpvmasumlem  27470  mudivsum  27513  selberglem1  27528  selberglem2  27529  selberg2lem  27533  selberg2  27534  pntrsumo1  27548  selbergr  27551  iscgrg  28600  isismt  28622  ishlg  28690  ishpg  28847  iscgra  28897  isinag  28926  isleag  28935  wksv  29709  sspval  30815  ajfval  30901  shex  31304  chex  31318  hmopex  31967  ressplusf  33044  inftmrel  33262  isinftm  33263  esplymhp  33733  esplyfv1  33734  constrsuc  33904  dmvlsiga  34295  measbase  34363  ismeas  34365  isrnmeas  34366  faeval  34412  eulerpartlemmf  34541  eulerpartlemgvv  34542  signsplypnf  34716  signsply0  34717  afsval  34837  fineqvnttrclse  35290  kur14lem7  35416  kur14lem9  35418  satfvsuclem1  35563  fmlasuc0  35588  mppsval  35776  dfon2lem7  35991  colinearex  36264  poimirlem4  37967  heibor1lem  38152  rrnval  38170  lsatset  39458  lcvfbr  39488  cmtfvalN  39678  cvrfval  39736  lineset  40206  psubspset  40212  psubclsetN  40404  lautset  40550  pautsetN  40566  tendoset  41227  dicval  41644  ltex  42706  leex  42707  sn-isghm  43128  eldiophb  43211  pellexlem3  43285  pellexlem5  43287  onfrALTlem3VD  45339  modelaxreplem1  45431  rpex  45802  dmvolsal  46800  smfresal  47242  smfliminflem  47284  sectfn  49524  amgmlemALT  50298