Theorem ssexi 5292

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  abex  5296  zfausab  5302  ord3ex  5357  epse  5636  opabex  7212  opabresex2  7459  mptexw  7951  fvclex  7957  oprabex  7975  mpoexw  8077  tfrlem16  8407  fosetex  8872  f1osetex  8873  dffi3  9443  r0weon  10026  dfac3  10135  dfac5lem4  10140  dfac5lem4OLD  10142  dfac2b  10145  hsmexlem6  10445  domtriomlem  10456  axdc3lem  10464  ac6  10494  brdom7disj  10545  brdom6disj  10546  niex  10895  enqex  10936  npex  11000  nrex1  11078  enrex  11081  reex  11220  nnex  12246  zex  12597  qex  12977  ixxex  13373  ltweuz  13979  seqexw  14035  cshwsexa  14842  prmex  16696  prdsval  17469  prdsle  17476  sectfval  17764  sscpwex  17828  issubc  17848  isfunc  17877  fullfunc  17921  fthfunc  17922  isfull  17925  isfth  17929  ipoval  18540  letsr  18603  ressmulgnn  19059  nmznsg  19151  eqgfval  19159  isghm  19198  isghmOLD  19199  lpival  21285  xrsle  21350  znle  21497  cssval  21642  pjfval  21666  ltbval  22001  opsrle  22005  istopon  22850  dmtopon  22861  leordtval2  23150  lecldbas  23157  xkoopn  23527  xkouni  23537  xkoccn  23557  xkoco1cn  23595  xkoco2cn  23596  xkococn  23598  xkoinjcn  23625  uzrest  23835  ustfn  24140  ustn0  24159  isphtpc  24944  tcphex  25169  tchnmfval  25180  bcthlem1  25276  bcthlem5  25280  dyadmbl  25553  itg2seq  25695  aannenlem3  26290  psercn  26388  abelth  26403  vmadivsum  27445  rpvmasumlem  27450  mudivsum  27493  selberglem1  27508  selberglem2  27509  selberg2lem  27513  selberg2  27514  pntrsumo1  27528  selbergr  27531  iscgrg  28491  isismt  28513  ishlg  28581  ishpg  28738  iscgra  28788  isinag  28817  isleag  28826  wksv  29599  sspval  30704  ajfval  30790  shex  31193  chex  31207  hmopex  31856  ressplusf  32939  inftmrel  33178  isinftm  33179  constrsuc  33772  dmvlsiga  34160  measbase  34228  ismeas  34230  isrnmeas  34231  faeval  34277  eulerpartlemmf  34407  eulerpartlemgvv  34408  signsplypnf  34582  signsply0  34583  afsval  34703  kur14lem7  35234  kur14lem9  35236  satfvsuclem1  35381  fmlasuc0  35406  mppsval  35594  dfon2lem7  35807  colinearex  36078  poimirlem4  37648  heibor1lem  37833  rrnval  37851  lsatset  39008  lcvfbr  39038  cmtfvalN  39228  cvrfval  39286  lineset  39757  psubspset  39763  psubclsetN  39955  lautset  40101  pautsetN  40117  tendoset  40778  dicval  41195  ltex  42296  leex  42297  sn-isghm  42696  eldiophb  42780  pellexlem3  42854  pellexlem5  42856  onfrALTlem3VD  44911  modelaxreplem1  45003  rpex  45373  dmvolsal  46375  smfresal  46817  smfliminflem  46859  upwordsseti  46914  sectfn  48999  amgmlemALT  49667