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 2144  Vcvv 3456   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923

This theorem is referenced by:  abex  5284  zfausab  5290  ord3ex  5346  epse  5631  opabex  7206  opabresex2  7452  mptexw  7936  fvclex  7942  oprabex  7959  mpoexw  8061  tfrlem16  8366  fosetex  8841  f1osetex  8842  dffi3  9379  r0weon  9970  dfac3  10079  dfac5lem4  10084  dfac5lem4OLD  10086  dfac2b  10089  hsmexlem6  10390  domtriomlem  10401  axdc3lem  10409  ac6  10439  brdom7disj  10490  brdom6disj  10491  niex  10841  enqex  10882  npex  10946  nrex1  11024  enrex  11027  reex  11166  nnex  12218  zex  12579  qex  12964  ixxex  13362  ltweuz  13976  seqexw  14032  cshwsexa  14839  prmex  16713  prdsval  17486  prdsle  17493  xrsle  17636  sectfval  17786  sscpwex  17850  issubc  17870  isfunc  17899  fullfunc  17943  fthfunc  17944  isfull  17947  isfth  17951  ipoval  18564  letsr  18627  ressmulgnn  19120  nmznsg  19211  eqgfval  19219  isghm  19258  lpival  21396  znle  21590  cssval  21736  pjfval  21760  ltbval  22098  opsrle  22102  istopon  22974  dmtopon  22985  leordtval2  23274  lecldbas  23281  xkoopn  23651  xkouni  23661  xkoccn  23681  xkoco1cn  23719  xkoco2cn  23720  xkococn  23722  xkoinjcn  23749  uzrest  23959  ustfn  24264  ustn0  24283  isphtpc  25058  tcphex  25281  tchnmfval  25292  bcthlem1  25388  bcthlem5  25392  dyadmbl  25664  itg2seq  25806  aannenlem3  26396  psercn  26491  abelth  26506  vmadivsum  27548  rpvmasumlem  27553  mudivsum  27596  selberglem1  27611  selberglem2  27612  selberg2lem  27616  selberg2  27617  pntrsumo1  27631  selbergr  27634  iscgrg  28683  isismt  28705  ishlg  28773  ishpg  28934  iscgra  29005  isinag  29034  isleag  29043  wksv  29822  sspval  30928  ajfval  31014  shex  31417  chex  31431  hmopex  32080  ressplusf  33143  inftmrel  33362  isinftm  33363  esplymhp  33867  esplyfv1  33868  constrsuc  34037  dmvlsiga  34428  measbase  34496  ismeas  34498  isrnmeas  34499  faeval  34545  eulerpartlemmf  34674  eulerpartlemgvv  34675  signsplypnf  34846  signsply0  34847  afsval  34970  fineqvnttrclse  35424  kur14lem7  35567  kur14lem9  35569  satfvsuclem1  35714  fmlasuc0  35739  mppsval  35927  dfon2lem7  36142  colinearex  36415  poimirlem4  38128  heibor1lem  38313  rrnval  38331  lsatset  39619  lcvfbr  39649  cmtfvalN  39839  cvrfval  39897  lineset  40367  psubspset  40373  psubclsetN  40565  lautset  40711  pautsetN  40727  tendoset  41388  dicval  41805  ltex  42866  leex  42867  sn-isghm  43260  eldiophb  43343  pellexlem3  43413  pellexlem5  43415  onfrALTlem3VD  45467  modelaxreplem1  45559  rpex  45927  dmvolsal  46925  smfresal  47367  smfliminflem  47409  sectfn  49655  amgmlemALT  50429