Theorem ssexi 5252

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

Syntax hints:   ∈ wcel 2114  Vcvv 3427   ⊆ wss 3885

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 5220

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 3388  df-v 3429  df-in 3892  df-ss 3902

This theorem is referenced by:  abex  5256  zfausab  5262  ord3ex  5318  epse  5602  opabex  7164  opabresex2  7410  mptexw  7895  fvclex  7901  oprabex  7918  mpoexw  8020  tfrlem16  8321  fosetex  8794  f1osetex  8795  dffi3  9333  r0weon  9923  dfac3  10032  dfac5lem4  10037  dfac5lem4OLD  10039  dfac2b  10042  hsmexlem6  10342  domtriomlem  10353  axdc3lem  10361  ac6  10391  brdom7disj  10442  brdom6disj  10443  niex  10793  enqex  10834  npex  10898  nrex1  10976  enrex  10979  reex  11118  nnex  12169  zex  12522  qex  12900  ixxex  13298  ltweuz  13912  seqexw  13968  cshwsexa  14775  prmex  16635  prdsval  17407  prdsle  17414  xrsle  17557  sectfval  17707  sscpwex  17771  issubc  17791  isfunc  17820  fullfunc  17864  fthfunc  17865  isfull  17868  isfth  17872  ipoval  18485  letsr  18548  ressmulgnn  19041  nmznsg  19132  eqgfval  19140  isghm  19179  isghmOLD  19180  lpival  21311  znle  21505  cssval  21651  pjfval  21675  ltbval  22010  opsrle  22014  istopon  22865  dmtopon  22876  leordtval2  23165  lecldbas  23172  xkoopn  23542  xkouni  23552  xkoccn  23572  xkoco1cn  23610  xkoco2cn  23611  xkococn  23613  xkoinjcn  23640  uzrest  23850  ustfn  24155  ustn0  24174  isphtpc  24949  tcphex  25172  tchnmfval  25183  bcthlem1  25279  bcthlem5  25283  dyadmbl  25555  itg2seq  25697  aannenlem3  26284  psercn  26379  abelth  26394  vmadivsum  27433  rpvmasumlem  27438  mudivsum  27481  selberglem1  27496  selberglem2  27497  selberg2lem  27501  selberg2  27502  pntrsumo1  27516  selbergr  27519  iscgrg  28568  isismt  28590  ishlg  28658  ishpg  28815  iscgra  28865  isinag  28894  isleag  28903  wksv  29676  sspval  30782  ajfval  30868  shex  31271  chex  31285  hmopex  31934  ressplusf  33011  inftmrel  33229  isinftm  33230  esplymhp  33700  esplyfv1  33701  constrsuc  33870  dmvlsiga  34261  measbase  34329  ismeas  34331  isrnmeas  34332  faeval  34378  eulerpartlemmf  34507  eulerpartlemgvv  34508  signsplypnf  34682  signsply0  34683  afsval  34803  fineqvnttrclse  35256  kur14lem7  35382  kur14lem9  35384  satfvsuclem1  35529  fmlasuc0  35554  mppsval  35742  dfon2lem7  35957  colinearex  36230  poimirlem4  37933  heibor1lem  38118  rrnval  38136  lsatset  39424  lcvfbr  39454  cmtfvalN  39644  cvrfval  39702  lineset  40172  psubspset  40178  psubclsetN  40370  lautset  40516  pautsetN  40532  tendoset  41193  dicval  41610  ltex  42672  leex  42673  sn-isghm  43094  eldiophb  43177  pellexlem3  43247  pellexlem5  43249  onfrALTlem3VD  45301  modelaxreplem1  45393  rpex  45764  dmvolsal  46762  smfresal  47204  smfliminflem  47246  sectfn  49492  amgmlemALT  50266