Theorem ssexi 5190

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  zfausab  5197  ord3ex  5253  epse  5502  opabex  6960  mptexw  7636  fvclex  7642  oprabex  7659  mpoexw  7759  tfrlem16  8012  dffi3  8879  r0weon  9423  dfac3  9532  dfac5lem4  9537  dfac2b  9541  hsmexlem6  9842  domtriomlem  9853  axdc3lem  9861  ac6  9891  brdom7disj  9942  brdom6disj  9943  niex  10292  enqex  10333  npex  10397  nrex1  10475  enrex  10478  reex  10617  nnex  11631  zex  11978  qex  12348  ixxex  12737  ltweuz  13324  seqexw  13380  prmex  16011  prdsval  16720  prdsle  16727  sectfval  17013  sscpwex  17077  issubc  17097  isfunc  17126  fullfunc  17168  fthfunc  17169  isfull  17172  isfth  17176  ipoval  17756  letsr  17829  nmznsg  18312  eqgfval  18320  isghm  18350  lpival  20011  xrsle  20111  znle  20228  cssval  20371  pjfval  20395  ltbval  20711  opsrle  20715  istopon  21517  dmtopon  21528  leordtval2  21817  lecldbas  21824  xkoopn  22194  xkouni  22204  xkoccn  22224  xkoco1cn  22262  xkoco2cn  22263  xkococn  22265  xkoinjcn  22292  uzrest  22502  ustfn  22807  ustn0  22826  isphtpc  23599  tcphex  23821  tchnmfval  23832  bcthlem1  23928  bcthlem5  23932  dyadmbl  24204  itg2seq  24346  aannenlem3  24926  psercn  25021  abelth  25036  vmadivsum  26066  rpvmasumlem  26071  mudivsum  26114  selberglem1  26129  selberglem2  26130  selberg2lem  26134  selberg2  26135  pntrsumo1  26149  selbergr  26152  iscgrg  26306  isismt  26328  ishlg  26396  ishpg  26553  iscgra  26603  isinag  26632  isleag  26641  pthsfval  27510  spthsfval  27511  crcts  27577  cycls  27578  eupths  27985  sspval  28506  ajfval  28592  shex  28995  chex  29009  hmopex  29658  ressplusf  30663  ressmulgnn  30717  inftmrel  30859  isinftm  30860  dmvlsiga  31498  measbase  31566  ismeas  31568  isrnmeas  31569  faeval  31615  eulerpartlemmf  31743  eulerpartlemgvv  31744  signsplypnf  31930  signsply0  31931  afsval  32052  kur14lem7  32572  kur14lem9  32574  satfvsuclem1  32719  fmlasuc0  32744  mppsval  32932  dfon2lem7  33147  colinearex  33634  poimirlem4  35061  heibor1lem  35247  rrnval  35265  lsatset  36286  lcvfbr  36316  cmtfvalN  36506  cvrfval  36564  lineset  37034  psubspset  37040  psubclsetN  37232  lautset  37378  pautsetN  37394  tendoset  38055  dicval  38472  eldiophb  39698  pellexlem3  39772  pellexlem5  39774  onfrALTlem3VD  41593  dmvolsal  42986  smfresal  43420  smfliminflem  43461  amgmlemALT  45331