Theorem ssexi 5322

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3948

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 5299

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 3955  df-ss 3965

This theorem is referenced by:  zfausab  5330  ord3ex  5385  epse  5659  opabex  7219  opabresex2  7458  mptexw  7936  fvclex  7942  oprabex  7960  mpoexw  8062  tfrlem16  8390  fosetex  8849  f1osetex  8850  dffi3  9423  r0weon  10004  dfac3  10113  dfac5lem4  10118  dfac2b  10122  hsmexlem6  10423  domtriomlem  10434  axdc3lem  10442  ac6  10472  brdom7disj  10523  brdom6disj  10524  niex  10873  enqex  10914  npex  10978  nrex1  11056  enrex  11059  reex  11198  nnex  12215  zex  12564  qex  12942  ixxex  13332  ltweuz  13923  seqexw  13979  cshwsexa  14771  prmex  16611  prdsval  17398  prdsle  17405  sectfval  17695  sscpwex  17759  issubc  17782  isfunc  17811  fullfunc  17854  fthfunc  17855  isfull  17858  isfth  17862  ipoval  18480  letsr  18543  nmznsg  19043  eqgfval  19051  isghm  19087  lpival  20876  xrsle  20958  znle  21080  cssval  21227  pjfval  21253  ltbval  21590  opsrle  21594  istopon  22406  dmtopon  22417  leordtval2  22708  lecldbas  22715  xkoopn  23085  xkouni  23095  xkoccn  23115  xkoco1cn  23153  xkoco2cn  23154  xkococn  23156  xkoinjcn  23183  uzrest  23393  ustfn  23698  ustn0  23717  isphtpc  24502  tcphex  24726  tchnmfval  24737  bcthlem1  24833  bcthlem5  24837  dyadmbl  25109  itg2seq  25252  aannenlem3  25835  psercn  25930  abelth  25945  vmadivsum  26975  rpvmasumlem  26980  mudivsum  27023  selberglem1  27038  selberglem2  27039  selberg2lem  27043  selberg2  27044  pntrsumo1  27058  selbergr  27061  iscgrg  27753  isismt  27775  ishlg  27843  ishpg  28000  iscgra  28050  isinag  28079  isleag  28088  wksv  28866  sspval  29964  ajfval  30050  shex  30453  chex  30467  hmopex  31116  ressplusf  32115  ressmulgnn  32172  inftmrel  32314  isinftm  32315  dmvlsiga  33116  measbase  33184  ismeas  33186  isrnmeas  33187  faeval  33233  eulerpartlemmf  33363  eulerpartlemgvv  33364  signsplypnf  33550  signsply0  33551  afsval  33672  kur14lem7  34192  kur14lem9  34194  satfvsuclem1  34339  fmlasuc0  34364  mppsval  34552  dfon2lem7  34750  colinearex  35021  poimirlem4  36481  heibor1lem  36666  rrnval  36684  lsatset  37849  lcvfbr  37879  cmtfvalN  38069  cvrfval  38127  lineset  38598  psubspset  38604  psubclsetN  38796  lautset  38942  pautsetN  38958  tendoset  39619  dicval  40036  eldiophb  41481  pellexlem3  41555  pellexlem5  41557  onfrALTlem3VD  43634  dmvolsal  45049  smfresal  45491  smfliminflem  45533  upwordsseti  45586  amgmlemALT  47804