Theorem ssexi 5261

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  abex  5265  zfausab  5271  ord3ex  5326  epse  5601  opabex  7156  opabresex2  7403  mptexw  7888  fvclex  7894  oprabex  7911  mpoexw  8013  tfrlem16  8315  fosetex  8785  f1osetex  8786  dffi3  9321  r0weon  9906  dfac3  10015  dfac5lem4  10020  dfac5lem4OLD  10022  dfac2b  10025  hsmexlem6  10325  domtriomlem  10336  axdc3lem  10344  ac6  10374  brdom7disj  10425  brdom6disj  10426  niex  10775  enqex  10816  npex  10880  nrex1  10958  enrex  10961  reex  11100  nnex  12134  zex  12480  qex  12862  ixxex  13259  ltweuz  13868  seqexw  13924  cshwsexa  14730  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  18955  nmznsg  19047  eqgfval  19055  isghm  19094  isghmOLD  19095  lpival  21231  znle  21443  cssval  21589  pjfval  21613  ltbval  21948  opsrle  21952  istopon  22797  dmtopon  22808  leordtval2  23097  lecldbas  23104  xkoopn  23474  xkouni  23484  xkoccn  23504  xkoco1cn  23542  xkoco2cn  23543  xkococn  23545  xkoinjcn  23572  uzrest  23782  ustfn  24087  ustn0  24106  isphtpc  24891  tcphex  25115  tchnmfval  25126  bcthlem1  25222  bcthlem5  25226  dyadmbl  25499  itg2seq  25641  aannenlem3  26236  psercn  26334  abelth  26349  vmadivsum  27391  rpvmasumlem  27396  mudivsum  27439  selberglem1  27454  selberglem2  27455  selberg2lem  27459  selberg2  27460  pntrsumo1  27474  selbergr  27477  iscgrg  28461  isismt  28483  ishlg  28551  ishpg  28708  iscgra  28758  isinag  28787  isleag  28796  wksv  29569  sspval  30671  ajfval  30757  shex  31160  chex  31174  hmopex  31823  ressplusf  32914  inftmrel  33131  isinftm  33132  constrsuc  33721  dmvlsiga  34112  measbase  34180  ismeas  34182  isrnmeas  34183  faeval  34229  eulerpartlemmf  34359  eulerpartlemgvv  34360  signsplypnf  34534  signsply0  34535  afsval  34655  fineqvnttrclse  35093  kur14lem7  35205  kur14lem9  35207  satfvsuclem1  35352  fmlasuc0  35377  mppsval  35565  dfon2lem7  35783  colinearex  36054  poimirlem4  37624  heibor1lem  37809  rrnval  37827  lsatset  38989  lcvfbr  39019  cmtfvalN  39209  cvrfval  39267  lineset  39737  psubspset  39743  psubclsetN  39935  lautset  40081  pautsetN  40097  tendoset  40758  dicval  41175  ltex  42238  leex  42239  sn-isghm  42666  eldiophb  42750  pellexlem3  42824  pellexlem5  42826  onfrALTlem3VD  44880  modelaxreplem1  44972  rpex  45346  dmvolsal  46347  smfresal  46789  smfliminflem  46831  upwordsseti  46886  sectfn  49034  amgmlemALT  49808