Theorem ssexi 5268

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

Syntax hints:   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902

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 5242

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 3401  df-v 3443  df-in 3909  df-ss 3919

This theorem is referenced by:  abex  5272  zfausab  5278  ord3ex  5333  epse  5607  opabex  7168  opabresex2  7414  mptexw  7899  fvclex  7905  oprabex  7922  mpoexw  8024  tfrlem16  8326  fosetex  8799  f1osetex  8800  dffi3  9338  r0weon  9926  dfac3  10035  dfac5lem4  10040  dfac5lem4OLD  10042  dfac2b  10045  hsmexlem6  10345  domtriomlem  10356  axdc3lem  10364  ac6  10394  brdom7disj  10445  brdom6disj  10446  niex  10796  enqex  10837  npex  10901  nrex1  10979  enrex  10982  reex  11121  nnex  12155  zex  12501  qex  12878  ixxex  13276  ltweuz  13888  seqexw  13944  cshwsexa  14751  prmex  16608  prdsval  17379  prdsle  17386  xrsle  17529  sectfval  17679  sscpwex  17743  issubc  17763  isfunc  17792  fullfunc  17836  fthfunc  17837  isfull  17840  isfth  17844  ipoval  18457  letsr  18520  ressmulgnn  19010  nmznsg  19101  eqgfval  19109  isghm  19148  isghmOLD  19149  lpival  21283  znle  21495  cssval  21641  pjfval  21665  ltbval  22002  opsrle  22006  istopon  22860  dmtopon  22871  leordtval2  23160  lecldbas  23167  xkoopn  23537  xkouni  23547  xkoccn  23567  xkoco1cn  23605  xkoco2cn  23606  xkococn  23608  xkoinjcn  23635  uzrest  23845  ustfn  24150  ustn0  24169  isphtpc  24953  tcphex  25177  tchnmfval  25188  bcthlem1  25284  bcthlem5  25288  dyadmbl  25561  itg2seq  25703  aannenlem3  26298  psercn  26396  abelth  26411  vmadivsum  27453  rpvmasumlem  27458  mudivsum  27501  selberglem1  27516  selberglem2  27517  selberg2lem  27521  selberg2  27522  pntrsumo1  27536  selbergr  27539  iscgrg  28588  isismt  28610  ishlg  28678  ishpg  28835  iscgra  28885  isinag  28914  isleag  28923  wksv  29697  sspval  30802  ajfval  30888  shex  31291  chex  31305  hmopex  31954  ressplusf  33047  inftmrel  33264  isinftm  33265  esplymhp  33728  esplyfv1  33729  constrsuc  33897  dmvlsiga  34288  measbase  34356  ismeas  34358  isrnmeas  34359  faeval  34405  eulerpartlemmf  34534  eulerpartlemgvv  34535  signsplypnf  34709  signsply0  34710  afsval  34830  fineqvnttrclse  35282  kur14lem7  35408  kur14lem9  35410  satfvsuclem1  35555  fmlasuc0  35580  mppsval  35768  dfon2lem7  35983  colinearex  36256  poimirlem4  37827  heibor1lem  38012  rrnval  38030  lsatset  39318  lcvfbr  39348  cmtfvalN  39538  cvrfval  39596  lineset  40066  psubspset  40072  psubclsetN  40264  lautset  40410  pautsetN  40426  tendoset  41087  dicval  41504  ltex  42567  leex  42568  sn-isghm  42983  eldiophb  43066  pellexlem3  43140  pellexlem5  43142  onfrALTlem3VD  45194  modelaxreplem1  45286  rpex  45658  dmvolsal  46657  smfresal  47099  smfliminflem  47141  sectfn  49341  amgmlemALT  50115