Theorem ssexi 5258

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  abex  5262  zfausab  5268  ord3ex  5323  epse  5596  opabex  7154  opabresex2  7400  mptexw  7885  fvclex  7891  oprabex  7908  mpoexw  8010  tfrlem16  8312  fosetex  8782  f1osetex  8783  dffi3  9315  r0weon  9903  dfac3  10012  dfac5lem4  10017  dfac5lem4OLD  10019  dfac2b  10022  hsmexlem6  10322  domtriomlem  10333  axdc3lem  10341  ac6  10371  brdom7disj  10422  brdom6disj  10423  niex  10772  enqex  10813  npex  10877  nrex1  10955  enrex  10958  reex  11097  nnex  12131  zex  12477  qex  12859  ixxex  13256  ltweuz  13868  seqexw  13924  cshwsexa  14731  prmex  16588  prdsval  17359  prdsle  17366  xrsle  17508  sectfval  17658  sscpwex  17722  issubc  17742  isfunc  17771  fullfunc  17815  fthfunc  17816  isfull  17819  isfth  17823  ipoval  18436  letsr  18499  ressmulgnn  18989  nmznsg  19080  eqgfval  19088  isghm  19127  isghmOLD  19128  lpival  21261  znle  21473  cssval  21619  pjfval  21643  ltbval  21978  opsrle  21982  istopon  22827  dmtopon  22838  leordtval2  23127  lecldbas  23134  xkoopn  23504  xkouni  23514  xkoccn  23534  xkoco1cn  23572  xkoco2cn  23573  xkococn  23575  xkoinjcn  23602  uzrest  23812  ustfn  24117  ustn0  24136  isphtpc  24920  tcphex  25144  tchnmfval  25155  bcthlem1  25251  bcthlem5  25255  dyadmbl  25528  itg2seq  25670  aannenlem3  26265  psercn  26363  abelth  26378  vmadivsum  27420  rpvmasumlem  27425  mudivsum  27468  selberglem1  27483  selberglem2  27484  selberg2lem  27488  selberg2  27489  pntrsumo1  27503  selbergr  27506  iscgrg  28490  isismt  28512  ishlg  28580  ishpg  28737  iscgra  28787  isinag  28816  isleag  28825  wksv  29598  sspval  30703  ajfval  30789  shex  31192  chex  31206  hmopex  31855  ressplusf  32944  inftmrel  33149  isinftm  33150  esplymhp  33589  esplyfv1  33590  constrsuc  33751  dmvlsiga  34142  measbase  34210  ismeas  34212  isrnmeas  34213  faeval  34259  eulerpartlemmf  34388  eulerpartlemgvv  34389  signsplypnf  34563  signsply0  34564  afsval  34684  fineqvnttrclse  35144  kur14lem7  35256  kur14lem9  35258  satfvsuclem1  35403  fmlasuc0  35428  mppsval  35616  dfon2lem7  35831  colinearex  36104  poimirlem4  37663  heibor1lem  37848  rrnval  37866  lsatset  39088  lcvfbr  39118  cmtfvalN  39308  cvrfval  39366  lineset  39836  psubspset  39842  psubclsetN  40034  lautset  40180  pautsetN  40196  tendoset  40857  dicval  41274  ltex  42337  leex  42338  sn-isghm  42765  eldiophb  42849  pellexlem3  42923  pellexlem5  42925  onfrALTlem3VD  44978  modelaxreplem1  45070  rpex  45444  dmvolsal  46443  smfresal  46885  smfliminflem  46927  sectfn  49129  amgmlemALT  49903