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  7177  opabresex2  7424  mptexw  7912  fvclex  7918  oprabex  7935  mpoexw  8037  tfrlem16  8339  fosetex  8809  f1osetex  8810  dffi3  9359  r0weon  9944  dfac3  10053  dfac5lem4  10058  dfac5lem4OLD  10060  dfac2b  10063  hsmexlem6  10363  domtriomlem  10374  axdc3lem  10382  ac6  10412  brdom7disj  10463  brdom6disj  10464  niex  10813  enqex  10854  npex  10918  nrex1  10996  enrex  10999  reex  11138  nnex  12171  zex  12517  qex  12899  ixxex  13296  ltweuz  13905  seqexw  13961  cshwsexa  14767  prmex  16625  prdsval  17396  prdsle  17403  xrsle  17545  sectfval  17695  sscpwex  17759  issubc  17779  isfunc  17808  fullfunc  17852  fthfunc  17853  isfull  17856  isfth  17860  ipoval  18473  letsr  18536  ressmulgnn  18992  nmznsg  19084  eqgfval  19092  isghm  19131  isghmOLD  19132  lpival  21268  znle  21480  cssval  21626  pjfval  21650  ltbval  21985  opsrle  21989  istopon  22834  dmtopon  22845  leordtval2  23134  lecldbas  23141  xkoopn  23511  xkouni  23521  xkoccn  23541  xkoco1cn  23579  xkoco2cn  23580  xkococn  23582  xkoinjcn  23609  uzrest  23819  ustfn  24124  ustn0  24143  isphtpc  24928  tcphex  25152  tchnmfval  25163  bcthlem1  25259  bcthlem5  25263  dyadmbl  25536  itg2seq  25678  aannenlem3  26273  psercn  26371  abelth  26386  vmadivsum  27428  rpvmasumlem  27433  mudivsum  27476  selberglem1  27491  selberglem2  27492  selberg2lem  27496  selberg2  27497  pntrsumo1  27511  selbergr  27514  iscgrg  28494  isismt  28516  ishlg  28584  ishpg  28741  iscgra  28791  isinag  28820  isleag  28829  wksv  29602  sspval  30704  ajfval  30790  shex  31193  chex  31207  hmopex  31856  ressplusf  32937  inftmrel  33151  isinftm  33152  constrsuc  33723  dmvlsiga  34114  measbase  34182  ismeas  34184  isrnmeas  34185  faeval  34231  eulerpartlemmf  34361  eulerpartlemgvv  34362  signsplypnf  34536  signsply0  34537  afsval  34657  kur14lem7  35194  kur14lem9  35196  satfvsuclem1  35341  fmlasuc0  35366  mppsval  35554  dfon2lem7  35772  colinearex  36043  poimirlem4  37613  heibor1lem  37798  rrnval  37816  lsatset  38978  lcvfbr  39008  cmtfvalN  39198  cvrfval  39256  lineset  39727  psubspset  39733  psubclsetN  39925  lautset  40071  pautsetN  40087  tendoset  40748  dicval  41165  ltex  42228  leex  42229  sn-isghm  42656  eldiophb  42740  pellexlem3  42814  pellexlem5  42816  onfrALTlem3VD  44871  modelaxreplem1  44963  rpex  45337  dmvolsal  46339  smfresal  46781  smfliminflem  46823  upwordsseti  46878  sectfn  49013  amgmlemALT  49787