Theorem ssexi 5327

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  abex  5331  zfausab  5337  ord3ex  5392  epse  5670  opabex  7239  opabresex2  7484  mptexw  7975  fvclex  7981  oprabex  7999  mpoexw  8101  tfrlem16  8431  fosetex  8896  f1osetex  8897  dffi3  9468  r0weon  10049  dfac3  10158  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2b  10168  hsmexlem6  10468  domtriomlem  10479  axdc3lem  10487  ac6  10517  brdom7disj  10568  brdom6disj  10569  niex  10918  enqex  10959  npex  11023  nrex1  11101  enrex  11104  reex  11243  nnex  12269  zex  12619  qex  13000  ixxex  13394  ltweuz  13998  seqexw  14054  cshwsexa  14858  prmex  16710  prdsval  17501  prdsle  17508  sectfval  17798  sscpwex  17862  issubc  17885  isfunc  17914  fullfunc  17959  fthfunc  17960  isfull  17963  isfth  17967  ipoval  18587  letsr  18650  ressmulgnn  19106  nmznsg  19198  eqgfval  19206  isghm  19245  isghmOLD  19246  lpival  21351  xrsle  21417  znle  21568  cssval  21717  pjfval  21743  ltbval  22078  opsrle  22082  istopon  22933  dmtopon  22944  leordtval2  23235  lecldbas  23242  xkoopn  23612  xkouni  23622  xkoccn  23642  xkoco1cn  23680  xkoco2cn  23681  xkococn  23683  xkoinjcn  23710  uzrest  23920  ustfn  24225  ustn0  24244  isphtpc  25039  tcphex  25264  tchnmfval  25275  bcthlem1  25371  bcthlem5  25375  dyadmbl  25648  itg2seq  25791  aannenlem3  26386  psercn  26484  abelth  26499  vmadivsum  27540  rpvmasumlem  27545  mudivsum  27588  selberglem1  27603  selberglem2  27604  selberg2lem  27608  selberg2  27609  pntrsumo1  27623  selbergr  27626  iscgrg  28534  isismt  28556  ishlg  28624  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  wksv  29651  sspval  30751  ajfval  30837  shex  31240  chex  31254  hmopex  31903  ressplusf  32932  inftmrel  33169  isinftm  33170  constrsuc  33742  dmvlsiga  34109  measbase  34177  ismeas  34179  isrnmeas  34180  faeval  34226  eulerpartlemmf  34356  eulerpartlemgvv  34357  signsplypnf  34543  signsply0  34544  afsval  34664  kur14lem7  35196  kur14lem9  35198  satfvsuclem1  35343  fmlasuc0  35368  mppsval  35556  dfon2lem7  35770  colinearex  36041  poimirlem4  37610  heibor1lem  37795  rrnval  37813  lsatset  38971  lcvfbr  39001  cmtfvalN  39191  cvrfval  39249  lineset  39720  psubspset  39726  psubclsetN  39918  lautset  40064  pautsetN  40080  tendoset  40741  dicval  41158  ltex  42264  leex  42265  sn-isghm  42659  eldiophb  42744  pellexlem3  42818  pellexlem5  42820  onfrALTlem3VD  44884  modelaxreplem1  44942  rpex  45295  dmvolsal  46301  smfresal  46743  smfliminflem  46785  upwordsseti  46838  amgmlemALT  49033