Theorem ssexi 5271

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903

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 2709  ax-sep 5245

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  abex  5275  zfausab  5281  ord3ex  5336  epse  5616  opabex  7178  opabresex2  7424  mptexw  7909  fvclex  7915  oprabex  7932  mpoexw  8034  tfrlem16  8336  fosetex  8809  f1osetex  8810  dffi3  9348  r0weon  9936  dfac3  10045  dfac5lem4  10050  dfac5lem4OLD  10052  dfac2b  10055  hsmexlem6  10355  domtriomlem  10366  axdc3lem  10374  ac6  10404  brdom7disj  10455  brdom6disj  10456  niex  10806  enqex  10847  npex  10911  nrex1  10989  enrex  10992  reex  11131  nnex  12165  zex  12511  qex  12888  ixxex  13286  ltweuz  13898  seqexw  13954  cshwsexa  14761  prmex  16618  prdsval  17389  prdsle  17396  xrsle  17539  sectfval  17689  sscpwex  17753  issubc  17773  isfunc  17802  fullfunc  17846  fthfunc  17847  isfull  17850  isfth  17854  ipoval  18467  letsr  18530  ressmulgnn  19023  nmznsg  19114  eqgfval  19122  isghm  19161  isghmOLD  19162  lpival  21296  znle  21508  cssval  21654  pjfval  21678  ltbval  22015  opsrle  22019  istopon  22873  dmtopon  22884  leordtval2  23173  lecldbas  23180  xkoopn  23550  xkouni  23560  xkoccn  23580  xkoco1cn  23618  xkoco2cn  23619  xkococn  23621  xkoinjcn  23648  uzrest  23858  ustfn  24163  ustn0  24182  isphtpc  24966  tcphex  25190  tchnmfval  25201  bcthlem1  25297  bcthlem5  25301  dyadmbl  25574  itg2seq  25716  aannenlem3  26311  psercn  26409  abelth  26424  vmadivsum  27466  rpvmasumlem  27471  mudivsum  27514  selberglem1  27529  selberglem2  27530  selberg2lem  27534  selberg2  27535  pntrsumo1  27549  selbergr  27552  iscgrg  28602  isismt  28624  ishlg  28692  ishpg  28849  iscgra  28899  isinag  28928  isleag  28937  wksv  29711  sspval  30817  ajfval  30903  shex  31306  chex  31320  hmopex  31969  ressplusf  33062  inftmrel  33280  isinftm  33281  esplymhp  33751  esplyfv1  33752  constrsuc  33922  dmvlsiga  34313  measbase  34381  ismeas  34383  isrnmeas  34384  faeval  34430  eulerpartlemmf  34559  eulerpartlemgvv  34560  signsplypnf  34734  signsply0  34735  afsval  34855  fineqvnttrclse  35308  kur14lem7  35434  kur14lem9  35436  satfvsuclem1  35581  fmlasuc0  35606  mppsval  35794  dfon2lem7  36009  colinearex  36282  poimirlem4  37904  heibor1lem  38089  rrnval  38107  lsatset  39395  lcvfbr  39425  cmtfvalN  39615  cvrfval  39673  lineset  40143  psubspset  40149  psubclsetN  40341  lautset  40487  pautsetN  40503  tendoset  41164  dicval  41581  ltex  42644  leex  42645  sn-isghm  43060  eldiophb  43143  pellexlem3  43217  pellexlem5  43219  onfrALTlem3VD  45271  modelaxreplem1  45363  rpex  45734  dmvolsal  46733  smfresal  47175  smfliminflem  47217  sectfn  49417  amgmlemALT  50191