Theorem ssexi 5321

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  zfausab  5329  ord3ex  5384  epse  5658  opabex  7218  opabresex2  7457  mptexw  7935  fvclex  7941  oprabex  7959  mpoexw  8061  tfrlem16  8389  fosetex  8848  f1osetex  8849  dffi3  9422  r0weon  10003  dfac3  10112  dfac5lem4  10117  dfac2b  10121  hsmexlem6  10422  domtriomlem  10433  axdc3lem  10441  ac6  10471  brdom7disj  10522  brdom6disj  10523  niex  10872  enqex  10913  npex  10977  nrex1  11055  enrex  11058  reex  11197  nnex  12214  zex  12563  qex  12941  ixxex  13331  ltweuz  13922  seqexw  13978  cshwsexa  14770  prmex  16610  prdsval  17397  prdsle  17404  sectfval  17694  sscpwex  17758  issubc  17781  isfunc  17810  fullfunc  17853  fthfunc  17854  isfull  17857  isfth  17861  ipoval  18479  letsr  18542  nmznsg  19042  eqgfval  19050  isghm  19086  lpival  20875  xrsle  20957  znle  21079  cssval  21226  pjfval  21252  ltbval  21589  opsrle  21593  istopon  22405  dmtopon  22416  leordtval2  22707  lecldbas  22714  xkoopn  23084  xkouni  23094  xkoccn  23114  xkoco1cn  23152  xkoco2cn  23153  xkococn  23155  xkoinjcn  23182  uzrest  23392  ustfn  23697  ustn0  23716  isphtpc  24501  tcphex  24725  tchnmfval  24736  bcthlem1  24832  bcthlem5  24836  dyadmbl  25108  itg2seq  25251  aannenlem3  25834  psercn  25929  abelth  25944  vmadivsum  26974  rpvmasumlem  26979  mudivsum  27022  selberglem1  27037  selberglem2  27038  selberg2lem  27042  selberg2  27043  pntrsumo1  27057  selbergr  27060  iscgrg  27752  isismt  27774  ishlg  27842  ishpg  27999  iscgra  28049  isinag  28078  isleag  28087  wksv  28865  sspval  29963  ajfval  30049  shex  30452  chex  30466  hmopex  31115  ressplusf  32114  ressmulgnn  32171  inftmrel  32313  isinftm  32314  dmvlsiga  33115  measbase  33183  ismeas  33185  isrnmeas  33186  faeval  33232  eulerpartlemmf  33362  eulerpartlemgvv  33363  signsplypnf  33549  signsply0  33550  afsval  33671  kur14lem7  34191  kur14lem9  34193  satfvsuclem1  34338  fmlasuc0  34363  mppsval  34551  dfon2lem7  34749  colinearex  35020  poimirlem4  36480  heibor1lem  36665  rrnval  36683  lsatset  37848  lcvfbr  37878  cmtfvalN  38068  cvrfval  38126  lineset  38597  psubspset  38603  psubclsetN  38795  lautset  38941  pautsetN  38957  tendoset  39618  dicval  40035  eldiophb  41480  pellexlem3  41554  pellexlem5  41556  onfrALTlem3VD  43633  dmvolsal  45048  smfresal  45490  smfliminflem  45532  upwordsseti  45585  amgmlemALT  47803