Theorem ssexi 5293

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

Syntax hints:   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928

This theorem is referenced by:  abex  5297  ord3ex  5359  epse  5644  opabex  7219  opabresex2  7465  mptexw  7950  fvclex  7956  oprabex  7973  mpoexw  8075  tfrlem16  8380  fosetex  8855  f1osetex  8856  dffi3  9391  r0weon  9996  dfac3  10105  dfac5lem4  10110  dfac2b  10114  hsmexlem6  10415  domtriomlem  10426  axdc3lem  10434  ac6  10464  brdom7disj  10515  brdom6disj  10516  niex  10866  enqex  10907  npex  10971  nrex1  11049  enrex  11052  reex  11191  nnex  12239  zex  12600  qex  12985  ixxex  13383  ltweuz  13997  seqexw  14053  cshwsexa  14861  prmex  16735  prdsval  17508  prdsle  17515  xrsle  17658  sectfval  17808  sscpwex  17872  issubc  17892  isfunc  17921  fullfunc  17965  fthfunc  17966  isfull  17969  isfth  17973  ipoval  18586  letsr  18649  ressmulgnn  19142  nmznsg  19234  eqgfval  19244  isghm  19286  lpival  21461  znle  21655  cssval  21801  pjfval  21825  ltbval  22163  opsrle  22167  istopon  23038  dmtopon  23049  leordtval2  23338  lecldbas  23345  xkoopn  23715  xkouni  23725  xkoccn  23745  xkoco1cn  23783  xkoco2cn  23784  xkococn  23786  xkoinjcn  23813  uzrest  24023  ustfn  24328  ustn0  24347  isphtpc  25122  tcphex  25345  tchnmfval  25356  bcthlem1  25452  bcthlem5  25456  dyadmbl  25728  itg2seq  25870  aannenlem3  26460  psercn  26555  abelth  26570  vmadivsum  27612  rpvmasumlem  27617  mudivsum  27660  selberglem1  27675  selberglem2  27676  selberg2lem  27680  selberg2  27681  pntrsumo1  27695  selbergr  27698  iscgrg  28747  isismt  28769  ishlg  28837  ishpg  29000  iscgra  29077  isinag  29110  isleag  29119  wksv  29910  sspval  31016  ajfval  31102  shex  31505  chex  31519  hmopex  32168  ressplusf  33224  inftmrel  33441  isinftm  33442  esplymhp  33903  esplyfv1  33904  constrsuc  34073  dmvlsiga  34464  measbase  34532  ismeas  34534  isrnmeas  34535  faeval  34581  eulerpartlemmf  34710  eulerpartlemgvv  34711  signsplypnf  34882  signsply0  34883  afsval  35006  fineqvnttrclse  35470  kur14lem7  35637  kur14lem9  35639  satfvsuclem1  35784  fmlasuc0  35809  mppsval  35997  dfon2lem7  36212  colinearex  36485  poimirlem4  38198  heibor1lem  38383  rrnval  38401  lsatset  39689  lcvfbr  39719  cmtfvalN  39909  cvrfval  39967  lineset  40437  psubspset  40443  psubclsetN  40635  lautset  40781  pautsetN  40797  tendoset  41458  dicval  41875  ltex  42938  leex  42939  sn-isghm  43332  eldiophb  43415  pellexlem3  43485  pellexlem5  43487  onfrALTlem3VD  45522  modelaxreplem1  45614  rpex  45989  dmvolsal  46987  smfresal  47429  smfliminflem  47471  sectfn  49727  amgmlemALT  50512