Theorem ssexi 5280

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  abex  5284  zfausab  5290  ord3ex  5345  epse  5623  opabex  7197  opabresex2  7444  mptexw  7934  fvclex  7940  oprabex  7958  mpoexw  8060  tfrlem16  8364  fosetex  8834  f1osetex  8835  dffi3  9389  r0weon  9972  dfac3  10081  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2b  10091  hsmexlem6  10391  domtriomlem  10402  axdc3lem  10410  ac6  10440  brdom7disj  10491  brdom6disj  10492  niex  10841  enqex  10882  npex  10946  nrex1  11024  enrex  11027  reex  11166  nnex  12199  zex  12545  qex  12927  ixxex  13324  ltweuz  13933  seqexw  13989  cshwsexa  14796  prmex  16654  prdsval  17425  prdsle  17432  sectfval  17720  sscpwex  17784  issubc  17804  isfunc  17833  fullfunc  17877  fthfunc  17878  isfull  17881  isfth  17885  ipoval  18496  letsr  18559  ressmulgnn  19015  nmznsg  19107  eqgfval  19115  isghm  19154  isghmOLD  19155  lpival  21241  xrsle  21306  znle  21453  cssval  21598  pjfval  21622  ltbval  21957  opsrle  21961  istopon  22806  dmtopon  22817  leordtval2  23106  lecldbas  23113  xkoopn  23483  xkouni  23493  xkoccn  23513  xkoco1cn  23551  xkoco2cn  23552  xkococn  23554  xkoinjcn  23581  uzrest  23791  ustfn  24096  ustn0  24115  isphtpc  24900  tcphex  25124  tchnmfval  25135  bcthlem1  25231  bcthlem5  25235  dyadmbl  25508  itg2seq  25650  aannenlem3  26245  psercn  26343  abelth  26358  vmadivsum  27400  rpvmasumlem  27405  mudivsum  27448  selberglem1  27463  selberglem2  27464  selberg2lem  27468  selberg2  27469  pntrsumo1  27483  selbergr  27486  iscgrg  28446  isismt  28468  ishlg  28536  ishpg  28693  iscgra  28743  isinag  28772  isleag  28781  wksv  29554  sspval  30659  ajfval  30745  shex  31148  chex  31162  hmopex  31811  ressplusf  32892  inftmrel  33141  isinftm  33142  constrsuc  33735  dmvlsiga  34126  measbase  34194  ismeas  34196  isrnmeas  34197  faeval  34243  eulerpartlemmf  34373  eulerpartlemgvv  34374  signsplypnf  34548  signsply0  34549  afsval  34669  kur14lem7  35206  kur14lem9  35208  satfvsuclem1  35353  fmlasuc0  35378  mppsval  35566  dfon2lem7  35784  colinearex  36055  poimirlem4  37625  heibor1lem  37810  rrnval  37828  lsatset  38990  lcvfbr  39020  cmtfvalN  39210  cvrfval  39268  lineset  39739  psubspset  39745  psubclsetN  39937  lautset  40083  pautsetN  40099  tendoset  40760  dicval  41177  ltex  42240  leex  42241  sn-isghm  42668  eldiophb  42752  pellexlem3  42826  pellexlem5  42828  onfrALTlem3VD  44883  modelaxreplem1  44975  rpex  45349  dmvolsal  46351  smfresal  46793  smfliminflem  46835  upwordsseti  46890  sectfn  49022  amgmlemALT  49796