Theorem ssexi 5322

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  abex  5326  zfausab  5332  ord3ex  5387  epse  5667  opabex  7240  opabresex2  7485  mptexw  7977  fvclex  7983  oprabex  8001  mpoexw  8103  tfrlem16  8433  fosetex  8898  f1osetex  8899  dffi3  9471  r0weon  10052  dfac3  10161  dfac5lem4  10166  dfac5lem4OLD  10168  dfac2b  10171  hsmexlem6  10471  domtriomlem  10482  axdc3lem  10490  ac6  10520  brdom7disj  10571  brdom6disj  10572  niex  10921  enqex  10962  npex  11026  nrex1  11104  enrex  11107  reex  11246  nnex  12272  zex  12622  qex  13003  ixxex  13398  ltweuz  14002  seqexw  14058  cshwsexa  14862  prmex  16714  prdsval  17500  prdsle  17507  sectfval  17795  sscpwex  17859  issubc  17880  isfunc  17909  fullfunc  17953  fthfunc  17954  isfull  17957  isfth  17961  ipoval  18575  letsr  18638  ressmulgnn  19094  nmznsg  19186  eqgfval  19194  isghm  19233  isghmOLD  19234  lpival  21334  xrsle  21400  znle  21551  cssval  21700  pjfval  21726  ltbval  22061  opsrle  22065  istopon  22918  dmtopon  22929  leordtval2  23220  lecldbas  23227  xkoopn  23597  xkouni  23607  xkoccn  23627  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  uzrest  23905  ustfn  24210  ustn0  24229  isphtpc  25026  tcphex  25251  tchnmfval  25262  bcthlem1  25358  bcthlem5  25362  dyadmbl  25635  itg2seq  25777  aannenlem3  26372  psercn  26470  abelth  26485  vmadivsum  27526  rpvmasumlem  27531  mudivsum  27574  selberglem1  27589  selberglem2  27590  selberg2lem  27594  selberg2  27595  pntrsumo1  27609  selbergr  27612  iscgrg  28520  isismt  28542  ishlg  28610  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  wksv  29637  sspval  30742  ajfval  30828  shex  31231  chex  31245  hmopex  31894  ressplusf  32948  inftmrel  33187  isinftm  33188  constrsuc  33779  dmvlsiga  34130  measbase  34198  ismeas  34200  isrnmeas  34201  faeval  34247  eulerpartlemmf  34377  eulerpartlemgvv  34378  signsplypnf  34565  signsply0  34566  afsval  34686  kur14lem7  35217  kur14lem9  35219  satfvsuclem1  35364  fmlasuc0  35389  mppsval  35577  dfon2lem7  35790  colinearex  36061  poimirlem4  37631  heibor1lem  37816  rrnval  37834  lsatset  38991  lcvfbr  39021  cmtfvalN  39211  cvrfval  39269  lineset  39740  psubspset  39746  psubclsetN  39938  lautset  40084  pautsetN  40100  tendoset  40761  dicval  41178  ltex  42286  leex  42287  sn-isghm  42683  eldiophb  42768  pellexlem3  42842  pellexlem5  42844  onfrALTlem3VD  44907  modelaxreplem1  44995  rpex  45357  dmvolsal  46361  smfresal  46803  smfliminflem  46845  upwordsseti  46900  amgmlemALT  49322