Theorem ssexi 5266

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

Syntax hints:   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917

This theorem is referenced by:  abex  5270  zfausab  5276  ord3ex  5331  epse  5605  opabex  7166  opabresex2  7412  mptexw  7897  fvclex  7903  oprabex  7920  mpoexw  8022  tfrlem16  8324  fosetex  8797  f1osetex  8798  dffi3  9336  r0weon  9924  dfac3  10033  dfac5lem4  10038  dfac5lem4OLD  10040  dfac2b  10043  hsmexlem6  10343  domtriomlem  10354  axdc3lem  10362  ac6  10392  brdom7disj  10443  brdom6disj  10444  niex  10794  enqex  10835  npex  10899  nrex1  10977  enrex  10980  reex  11119  nnex  12153  zex  12499  qex  12876  ixxex  13274  ltweuz  13886  seqexw  13942  cshwsexa  14749  prmex  16606  prdsval  17377  prdsle  17384  xrsle  17527  sectfval  17677  sscpwex  17741  issubc  17761  isfunc  17790  fullfunc  17834  fthfunc  17835  isfull  17838  isfth  17842  ipoval  18455  letsr  18518  ressmulgnn  19008  nmznsg  19099  eqgfval  19107  isghm  19146  isghmOLD  19147  lpival  21281  znle  21493  cssval  21639  pjfval  21663  ltbval  22000  opsrle  22004  istopon  22858  dmtopon  22869  leordtval2  23158  lecldbas  23165  xkoopn  23535  xkouni  23545  xkoccn  23565  xkoco1cn  23603  xkoco2cn  23604  xkococn  23606  xkoinjcn  23633  uzrest  23843  ustfn  24148  ustn0  24167  isphtpc  24951  tcphex  25175  tchnmfval  25186  bcthlem1  25282  bcthlem5  25286  dyadmbl  25559  itg2seq  25701  aannenlem3  26296  psercn  26394  abelth  26409  vmadivsum  27451  rpvmasumlem  27456  mudivsum  27499  selberglem1  27514  selberglem2  27515  selberg2lem  27519  selberg2  27520  pntrsumo1  27534  selbergr  27537  iscgrg  28565  isismt  28587  ishlg  28655  ishpg  28812  iscgra  28862  isinag  28891  isleag  28900  wksv  29674  sspval  30779  ajfval  30865  shex  31268  chex  31282  hmopex  31931  ressplusf  33024  inftmrel  33241  isinftm  33242  esplymhp  33705  esplyfv1  33706  constrsuc  33874  dmvlsiga  34265  measbase  34333  ismeas  34335  isrnmeas  34336  faeval  34382  eulerpartlemmf  34511  eulerpartlemgvv  34512  signsplypnf  34686  signsply0  34687  afsval  34807  fineqvnttrclse  35259  kur14lem7  35385  kur14lem9  35387  satfvsuclem1  35532  fmlasuc0  35557  mppsval  35745  dfon2lem7  35960  colinearex  36233  poimirlem4  37794  heibor1lem  37979  rrnval  37997  lsatset  39285  lcvfbr  39315  cmtfvalN  39505  cvrfval  39563  lineset  40033  psubspset  40039  psubclsetN  40231  lautset  40377  pautsetN  40393  tendoset  41054  dicval  41471  ltex  42537  leex  42538  sn-isghm  42953  eldiophb  43036  pellexlem3  43110  pellexlem5  43112  onfrALTlem3VD  45164  modelaxreplem1  45256  rpex  45628  dmvolsal  46627  smfresal  47069  smfliminflem  47111  sectfn  49311  amgmlemALT  50085