Theorem ssexi 5251

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5219

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  abex  5255  zfausab  5261  ord3ex  5317  epse  5601  opabex  7165  opabresex2  7411  mptexw  7896  fvclex  7902  oprabex  7919  mpoexw  8021  tfrlem16  8323  fosetex  8796  f1osetex  8797  dffi3  9335  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  12172  zex  12525  qex  12903  ixxex  13301  ltweuz  13915  seqexw  13971  cshwsexa  14778  prmex  16638  prdsval  17410  prdsle  17417  xrsle  17560  sectfval  17710  sscpwex  17774  issubc  17794  isfunc  17823  fullfunc  17867  fthfunc  17868  isfull  17871  isfth  17875  ipoval  18488  letsr  18551  ressmulgnn  19044  nmznsg  19135  eqgfval  19143  isghm  19182  isghmOLD  19183  lpival  21318  znle  21512  cssval  21658  pjfval  21682  ltbval  22020  opsrle  22024  istopon  22896  dmtopon  22907  leordtval2  23196  lecldbas  23203  xkoopn  23573  xkouni  23583  xkoccn  23603  xkoco1cn  23641  xkoco2cn  23642  xkococn  23644  xkoinjcn  23671  uzrest  23881  ustfn  24186  ustn0  24205  isphtpc  24980  tcphex  25203  tchnmfval  25214  bcthlem1  25310  bcthlem5  25314  dyadmbl  25586  itg2seq  25728  aannenlem3  26315  psercn  26410  abelth  26425  vmadivsum  27464  rpvmasumlem  27469  mudivsum  27512  selberglem1  27527  selberglem2  27528  selberg2lem  27532  selberg2  27533  pntrsumo1  27547  selbergr  27550  iscgrg  28599  isismt  28621  ishlg  28689  ishpg  28846  iscgra  28896  isinag  28925  isleag  28934  wksv  29707  sspval  30813  ajfval  30899  shex  31302  chex  31316  hmopex  31965  ressplusf  33043  inftmrel  33262  isinftm  33263  esplymhp  33761  esplyfv1  33762  constrsuc  33931  dmvlsiga  34322  measbase  34390  ismeas  34392  isrnmeas  34393  faeval  34439  eulerpartlemmf  34568  eulerpartlemgvv  34569  signsplypnf  34743  signsply0  34744  afsval  34864  fineqvnttrclse  35314  kur14lem7  35449  kur14lem9  35451  satfvsuclem1  35596  fmlasuc0  35621  mppsval  35809  dfon2lem7  36024  colinearex  36297  poimirlem4  38000  heibor1lem  38185  rrnval  38203  lsatset  39491  lcvfbr  39521  cmtfvalN  39711  cvrfval  39769  lineset  40239  psubspset  40245  psubclsetN  40437  lautset  40583  pautsetN  40599  tendoset  41260  dicval  41677  ltex  42738  leex  42739  sn-isghm  43132  eldiophb  43215  pellexlem3  43285  pellexlem5  43287  onfrALTlem3VD  45339  modelaxreplem1  45431  rpex  45799  dmvolsal  46797  smfresal  47239  smfliminflem  47281  sectfn  49527  amgmlemALT  50301