Theorem ssexi 5277

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  abex  5281  zfausab  5287  ord3ex  5342  epse  5620  opabex  7194  opabresex2  7441  mptexw  7931  fvclex  7937  oprabex  7955  mpoexw  8057  tfrlem16  8361  fosetex  8831  f1osetex  8832  dffi3  9382  r0weon  9965  dfac3  10074  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  hsmexlem6  10384  domtriomlem  10395  axdc3lem  10403  ac6  10433  brdom7disj  10484  brdom6disj  10485  niex  10834  enqex  10875  npex  10939  nrex1  11017  enrex  11020  reex  11159  nnex  12192  zex  12538  qex  12920  ixxex  13317  ltweuz  13926  seqexw  13982  cshwsexa  14789  prmex  16647  prdsval  17418  prdsle  17425  sectfval  17713  sscpwex  17777  issubc  17797  isfunc  17826  fullfunc  17870  fthfunc  17871  isfull  17874  isfth  17878  ipoval  18489  letsr  18552  ressmulgnn  19008  nmznsg  19100  eqgfval  19108  isghm  19147  isghmOLD  19148  lpival  21234  xrsle  21299  znle  21446  cssval  21591  pjfval  21615  ltbval  21950  opsrle  21954  istopon  22799  dmtopon  22810  leordtval2  23099  lecldbas  23106  xkoopn  23476  xkouni  23486  xkoccn  23506  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  uzrest  23784  ustfn  24089  ustn0  24108  isphtpc  24893  tcphex  25117  tchnmfval  25128  bcthlem1  25224  bcthlem5  25228  dyadmbl  25501  itg2seq  25643  aannenlem3  26238  psercn  26336  abelth  26351  vmadivsum  27393  rpvmasumlem  27398  mudivsum  27441  selberglem1  27456  selberglem2  27457  selberg2lem  27461  selberg2  27462  pntrsumo1  27476  selbergr  27479  iscgrg  28439  isismt  28461  ishlg  28529  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  wksv  29547  sspval  30652  ajfval  30738  shex  31141  chex  31155  hmopex  31804  ressplusf  32885  inftmrel  33134  isinftm  33135  constrsuc  33728  dmvlsiga  34119  measbase  34187  ismeas  34189  isrnmeas  34190  faeval  34236  eulerpartlemmf  34366  eulerpartlemgvv  34367  signsplypnf  34541  signsply0  34542  afsval  34662  kur14lem7  35199  kur14lem9  35201  satfvsuclem1  35346  fmlasuc0  35371  mppsval  35559  dfon2lem7  35777  colinearex  36048  poimirlem4  37618  heibor1lem  37803  rrnval  37821  lsatset  38983  lcvfbr  39013  cmtfvalN  39203  cvrfval  39261  lineset  39732  psubspset  39738  psubclsetN  39930  lautset  40076  pautsetN  40092  tendoset  40753  dicval  41170  ltex  42233  leex  42234  sn-isghm  42661  eldiophb  42745  pellexlem3  42819  pellexlem5  42821  onfrALTlem3VD  44876  modelaxreplem1  44968  rpex  45342  dmvolsal  46344  smfresal  46786  smfliminflem  46828  upwordsseti  46883  sectfn  49018  amgmlemALT  49792