Theorem ssexi 5292

Description: A subclass of a set is 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 5290	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921

This theorem is used by:  abex  5296  ord3ex  5357  epse  5642  opabex  7218  opabresex2  7466  mptexw  7948  fvclex  7954  oprabex  7971  mpoexw  8073  tfrlem16  8378  fosetex  8853  f1osetex  8854  dffi3  9389  r0weon  10003  dfac3  10112  dfac5lem4  10117  dfac2b  10121  hsmexlem6  10421  domtriomlem  10432  axdc3lem  10440  ac6  10470  brdom7disj  10521  brdom6disj  10522  niex  10872  enqex  10913  npex  10977  nrex1  11055  enrex  11058  reex  11197  nnex  12245  zex  12606  qex  12991  ixxex  13389  ltweuz  14004  seqexw  14060  cshwsexa  14868  prmex  16741  prdsval  17514  prdsle  17521  xrsle  17664  sectfval  17814  sscpwex  17878  issubc  17898  isfunc  17927  fullfunc  17971  fthfunc  17972  isfull  17975  isfth  17979  ipoval  18592  letsr  18655  ressmulgnn  19148  nmznsg  19240  eqgfval  19250  isghm  19292  lpival  21503  znle  21697  cssval  21843  pjfval  21867  ltbval  22205  opsrle  22209  istopon  23080  dmtopon  23091  leordtval2  23380  lecldbas  23387  xkoopn  23757  xkouni  23767  xkoccn  23787  xkoco1cn  23825  xkoco2cn  23826  xkococn  23828  xkoinjcn  23855  uzrest  24065  ustfn  24370  ustn0  24389  isphtpc  25164  tcphex  25387  tchnmfval  25398  bcthlem1  25494  bcthlem5  25498  dyadmbl  25770  itg2seq  25912  aannenlem3  26504  psercn  26600  abelth  26615  vmadivsum  27657  rpvmasumlem  27662  mudivsum  27705  selberglem1  27720  selberglem2  27721  selberg2lem  27725  selberg2  27726  pntrsumo1  27740  selbergr  27743  iscgrg  28792  isismt  28814  ishlg2  28882  ishlg  28885  ishpg  29052  iscgra  29131  isinag  29166  isleag  29175  wksv  29980  sspval  31086  ajfval  31172  shex  31575  chex  31589  hmopex  32238  ressplusf  33292  inftmrel  33509  isinftm  33510  esplymhp  33967  esplyfv1  33968  constrsuc  34137  dmvlsiga  34528  measbase  34596  ismeas  34598  isrnmeas  34599  faeval  34645  eulerpartlemmf  34774  eulerpartlemgvv  34775  signsplypnf  34946  signsply0  34947  afsval  35070  fineqvnttrclse  35545  kur14lem7  35712  kur14lem9  35714  satfvsuclem1  35859  fmlasuc0  35884  mppsval  36072  dfon2lem7  36287  colinearex  36560  poimirlem4  38303  heibor1lem  38488  rrnval  38506  lsatset  39792  lcvfbr  39822  cmtfvalN  40012  cvrfval  40070  lineset  40540  psubspset  40546  psubclsetN  40738  lautset  40884  pautsetN  40900  tendoset  41561  dicval  41978  ltex  43041  leex  43042  sn-isghm  43433  eldiophb  43516  pellexlem3  43586  pellexlem5  43588  onfrALTlem3VD  45623  modelaxreplem1  45715  rpex  46090  dmvolsal  47088  smfresal  47530  smfliminflem  47572  sectfn  49835  amgmlemALT  50678