Theorem ssexi 5340

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  abex  5344  zfausab  5350  ord3ex  5405  epse  5682  opabex  7257  opabresex2  7502  mptexw  7993  fvclex  7999  oprabex  8017  mpoexw  8119  tfrlem16  8449  fosetex  8916  f1osetex  8917  dffi3  9500  r0weon  10081  dfac3  10190  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  hsmexlem6  10500  domtriomlem  10511  axdc3lem  10519  ac6  10549  brdom7disj  10600  brdom6disj  10601  niex  10950  enqex  10991  npex  11055  nrex1  11133  enrex  11136  reex  11275  nnex  12299  zex  12648  qex  13026  ixxex  13418  ltweuz  14012  seqexw  14068  cshwsexa  14872  prmex  16724  prdsval  17515  prdsle  17522  sectfval  17812  sscpwex  17876  issubc  17899  isfunc  17928  fullfunc  17973  fthfunc  17974  isfull  17977  isfth  17981  ipoval  18600  letsr  18663  ressmulgnn  19116  nmznsg  19208  eqgfval  19216  isghm  19255  isghmOLD  19256  lpival  21357  xrsle  21423  znle  21574  cssval  21723  pjfval  21749  ltbval  22084  opsrle  22088  istopon  22939  dmtopon  22950  leordtval2  23241  lecldbas  23248  xkoopn  23618  xkouni  23628  xkoccn  23648  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  uzrest  23926  ustfn  24231  ustn0  24250  isphtpc  25045  tcphex  25270  tchnmfval  25281  bcthlem1  25377  bcthlem5  25381  dyadmbl  25654  itg2seq  25797  aannenlem3  26390  psercn  26488  abelth  26503  vmadivsum  27544  rpvmasumlem  27549  mudivsum  27592  selberglem1  27607  selberglem2  27608  selberg2lem  27612  selberg2  27613  pntrsumo1  27627  selbergr  27630  iscgrg  28538  isismt  28560  ishlg  28628  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  wksv  29655  sspval  30755  ajfval  30841  shex  31244  chex  31258  hmopex  31907  ressplusf  32930  inftmrel  33160  isinftm  33161  constrsuc  33728  dmvlsiga  34093  measbase  34161  ismeas  34163  isrnmeas  34164  faeval  34210  eulerpartlemmf  34340  eulerpartlemgvv  34341  signsplypnf  34527  signsply0  34528  afsval  34648  kur14lem7  35180  kur14lem9  35182  satfvsuclem1  35327  fmlasuc0  35352  mppsval  35540  dfon2lem7  35753  colinearex  36024  poimirlem4  37584  heibor1lem  37769  rrnval  37787  lsatset  38946  lcvfbr  38976  cmtfvalN  39166  cvrfval  39224  lineset  39695  psubspset  39701  psubclsetN  39893  lautset  40039  pautsetN  40055  tendoset  40716  dicval  41133  ltex  42240  leex  42241  sn-isghm  42628  eldiophb  42713  pellexlem3  42787  pellexlem5  42789  onfrALTlem3VD  44858  dmvolsal  46267  smfresal  46709  smfliminflem  46751  upwordsseti  46804  amgmlemALT  48897