Theorem ssexi 5323

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  zfausab  5331  ord3ex  5386  epse  5660  opabex  7222  opabresex2  7461  mptexw  7939  fvclex  7945  oprabex  7963  mpoexw  8065  tfrlem16  8393  fosetex  8852  f1osetex  8853  dffi3  9426  r0weon  10007  dfac3  10116  dfac5lem4  10121  dfac2b  10125  hsmexlem6  10426  domtriomlem  10437  axdc3lem  10445  ac6  10475  brdom7disj  10526  brdom6disj  10527  niex  10876  enqex  10917  npex  10981  nrex1  11059  enrex  11062  reex  11201  nnex  12218  zex  12567  qex  12945  ixxex  13335  ltweuz  13926  seqexw  13982  cshwsexa  14774  prmex  16614  prdsval  17401  prdsle  17408  sectfval  17698  sscpwex  17762  issubc  17785  isfunc  17814  fullfunc  17857  fthfunc  17858  isfull  17861  isfth  17865  ipoval  18483  letsr  18546  nmznsg  19048  eqgfval  19056  isghm  19092  lpival  20883  xrsle  20965  znle  21088  cssval  21235  pjfval  21261  ltbval  21598  opsrle  21602  istopon  22414  dmtopon  22425  leordtval2  22716  lecldbas  22723  xkoopn  23093  xkouni  23103  xkoccn  23123  xkoco1cn  23161  xkoco2cn  23162  xkococn  23164  xkoinjcn  23191  uzrest  23401  ustfn  23706  ustn0  23725  isphtpc  24510  tcphex  24734  tchnmfval  24745  bcthlem1  24841  bcthlem5  24845  dyadmbl  25117  itg2seq  25260  aannenlem3  25843  psercn  25938  abelth  25953  vmadivsum  26985  rpvmasumlem  26990  mudivsum  27033  selberglem1  27048  selberglem2  27049  selberg2lem  27053  selberg2  27054  pntrsumo1  27068  selbergr  27071  iscgrg  27763  isismt  27785  ishlg  27853  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  wksv  28876  sspval  29976  ajfval  30062  shex  30465  chex  30479  hmopex  31128  ressplusf  32127  ressmulgnn  32184  inftmrel  32326  isinftm  32327  dmvlsiga  33127  measbase  33195  ismeas  33197  isrnmeas  33198  faeval  33244  eulerpartlemmf  33374  eulerpartlemgvv  33375  signsplypnf  33561  signsply0  33562  afsval  33683  kur14lem7  34203  kur14lem9  34205  satfvsuclem1  34350  fmlasuc0  34375  mppsval  34563  dfon2lem7  34761  colinearex  35032  poimirlem4  36492  heibor1lem  36677  rrnval  36695  lsatset  37860  lcvfbr  37890  cmtfvalN  38080  cvrfval  38138  lineset  38609  psubspset  38615  psubclsetN  38807  lautset  38953  pautsetN  38969  tendoset  39630  dicval  40047  eldiophb  41495  pellexlem3  41569  pellexlem5  41571  onfrALTlem3VD  43648  dmvolsal  45062  smfresal  45504  smfliminflem  45546  upwordsseti  45599  amgmlemALT  47850