Theorem ssexi 5324

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

Syntax hints:   ∈ wcel 2098  Vcvv 3471   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-sep 5301

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  abex  5328  zfausab  5334  ord3ex  5389  epse  5663  opabex  7236  opabresex2  7476  mptexw  7960  fvclex  7966  oprabex  7984  mpoexw  8087  tfrlem16  8418  fosetex  8881  f1osetex  8882  dffi3  9460  r0weon  10041  dfac3  10150  dfac5lem4  10155  dfac2b  10159  hsmexlem6  10460  domtriomlem  10471  axdc3lem  10479  ac6  10509  brdom7disj  10560  brdom6disj  10561  niex  10910  enqex  10951  npex  11015  nrex1  11093  enrex  11096  reex  11235  nnex  12254  zex  12603  qex  12981  ixxex  13373  ltweuz  13964  seqexw  14020  cshwsexa  14812  prmex  16653  prdsval  17442  prdsle  17449  sectfval  17739  sscpwex  17803  issubc  17826  isfunc  17855  fullfunc  17900  fthfunc  17901  isfull  17904  isfth  17908  ipoval  18527  letsr  18590  ressmulgnn  19037  nmznsg  19128  eqgfval  19136  isghm  19175  lpival  21219  xrsle  21320  znle  21471  cssval  21619  pjfval  21645  ltbval  21986  opsrle  21990  istopon  22832  dmtopon  22843  leordtval2  23134  lecldbas  23141  xkoopn  23511  xkouni  23521  xkoccn  23541  xkoco1cn  23579  xkoco2cn  23580  xkococn  23582  xkoinjcn  23609  uzrest  23819  ustfn  24124  ustn0  24143  isphtpc  24938  tcphex  25163  tchnmfval  25174  bcthlem1  25270  bcthlem5  25274  dyadmbl  25547  itg2seq  25690  aannenlem3  26283  psercn  26381  abelth  26396  vmadivsum  27433  rpvmasumlem  27438  mudivsum  27481  selberglem1  27496  selberglem2  27497  selberg2lem  27501  selberg2  27502  pntrsumo1  27516  selbergr  27519  iscgrg  28334  isismt  28356  ishlg  28424  ishpg  28581  iscgra  28631  isinag  28660  isleag  28669  wksv  29451  sspval  30551  ajfval  30637  shex  31040  chex  31054  hmopex  31703  ressplusf  32702  inftmrel  32906  isinftm  32907  dmvlsiga  33753  measbase  33821  ismeas  33823  isrnmeas  33824  faeval  33870  eulerpartlemmf  34000  eulerpartlemgvv  34001  signsplypnf  34187  signsply0  34188  afsval  34308  kur14lem7  34827  kur14lem9  34829  satfvsuclem1  34974  fmlasuc0  34999  mppsval  35187  dfon2lem7  35390  colinearex  35661  poimirlem4  37102  heibor1lem  37287  rrnval  37305  lsatset  38466  lcvfbr  38496  cmtfvalN  38686  cvrfval  38744  lineset  39215  psubspset  39221  psubclsetN  39413  lautset  39559  pautsetN  39575  tendoset  40236  dicval  40653  eldiophb  42180  pellexlem3  42254  pellexlem5  42256  onfrALTlem3VD  44329  dmvolsal  45736  smfresal  46178  smfliminflem  46220  upwordsseti  46273  amgmlemALT  48287