Theorem ssexi 5272

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ⊆ 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  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  abex  5276  zfausab  5282  ord3ex  5337  epse  5613  opabex  7176  opabresex2  7423  mptexw  7911  fvclex  7917  oprabex  7934  mpoexw  8036  tfrlem16  8338  fosetex  8808  f1osetex  8809  dffi3  9358  r0weon  9943  dfac3  10052  dfac5lem4  10057  dfac5lem4OLD  10059  dfac2b  10062  hsmexlem6  10362  domtriomlem  10373  axdc3lem  10381  ac6  10411  brdom7disj  10462  brdom6disj  10463  niex  10812  enqex  10853  npex  10917  nrex1  10995  enrex  10998  reex  11137  nnex  12170  zex  12516  qex  12898  ixxex  13295  ltweuz  13904  seqexw  13960  cshwsexa  14766  prmex  16624  prdsval  17395  prdsle  17402  xrsle  17544  sectfval  17694  sscpwex  17758  issubc  17778  isfunc  17807  fullfunc  17851  fthfunc  17852  isfull  17855  isfth  17859  ipoval  18472  letsr  18535  ressmulgnn  18991  nmznsg  19083  eqgfval  19091  isghm  19130  isghmOLD  19131  lpival  21267  znle  21479  cssval  21625  pjfval  21649  ltbval  21984  opsrle  21988  istopon  22833  dmtopon  22844  leordtval2  23133  lecldbas  23140  xkoopn  23510  xkouni  23520  xkoccn  23540  xkoco1cn  23578  xkoco2cn  23579  xkococn  23581  xkoinjcn  23608  uzrest  23818  ustfn  24123  ustn0  24142  isphtpc  24927  tcphex  25151  tchnmfval  25162  bcthlem1  25258  bcthlem5  25262  dyadmbl  25535  itg2seq  25677  aannenlem3  26272  psercn  26370  abelth  26385  vmadivsum  27427  rpvmasumlem  27432  mudivsum  27475  selberglem1  27490  selberglem2  27491  selberg2lem  27495  selberg2  27496  pntrsumo1  27510  selbergr  27513  iscgrg  28493  isismt  28515  ishlg  28583  ishpg  28740  iscgra  28790  isinag  28819  isleag  28828  wksv  29601  sspval  30703  ajfval  30789  shex  31192  chex  31206  hmopex  31855  ressplusf  32936  inftmrel  33150  isinftm  33151  constrsuc  33722  dmvlsiga  34113  measbase  34181  ismeas  34183  isrnmeas  34184  faeval  34230  eulerpartlemmf  34360  eulerpartlemgvv  34361  signsplypnf  34535  signsply0  34536  afsval  34656  kur14lem7  35193  kur14lem9  35195  satfvsuclem1  35340  fmlasuc0  35365  mppsval  35553  dfon2lem7  35771  colinearex  36042  poimirlem4  37612  heibor1lem  37797  rrnval  37815  lsatset  38977  lcvfbr  39007  cmtfvalN  39197  cvrfval  39255  lineset  39726  psubspset  39732  psubclsetN  39924  lautset  40070  pautsetN  40086  tendoset  40747  dicval  41164  ltex  42227  leex  42228  sn-isghm  42655  eldiophb  42739  pellexlem3  42813  pellexlem5  42815  onfrALTlem3VD  44870  modelaxreplem1  44962  rpex  45336  dmvolsal  46338  smfresal  46780  smfliminflem  46822  upwordsseti  46877  sectfn  49012  amgmlemALT  49786