Theorem ssexi 5291

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  abex  5295  ord3ex  5356  epse  5641  opabex  7222  opabresex2  7470  mptexw  7953  fvclex  7959  oprabex  7976  mpoexw  8080  tfrlem16  8385  fosetex  8862  f1osetex  8863  dffi3  9404  r0weon  10018  dfac3  10127  dfac5lem4  10132  dfac2b  10136  hsmexlem6  10436  domtriomlem  10447  axdc3lem  10455  ac6  10485  brdom7disj  10537  brdom6disj  10538  niex  10893  enqex  10934  npex  10998  nrex1  11076  enrex  11079  reex  11218  nnex  12266  zex  12627  qex  13013  ixxex  13411  ltweuz  14027  seqexw  14083  cshwsexa  14897  prmex  16771  prdsval  17544  prdsle  17551  xrsle  17694  sectfval  17844  sscpwex  17908  issubc  17928  isfunc  17957  fullfunc  18001  fthfunc  18002  isfull  18005  isfth  18009  ipoval  18622  letsr  18685  ressmulgnn  19200  nmznsg  19292  eqgfval  19302  isghm  19344  lpival  21556  znle  21750  cssval  21896  pjfval  21920  ltbval  22260  opsrle  22264  istopon  23138  dmtopon  23149  leordtval2  23438  lecldbas  23445  xkoopn  23816  xkouni  23826  xkoccn  23846  xkoco1cn  23884  xkoco2cn  23885  xkococn  23887  xkoinjcn  23914  uzrest  24124  ustfn  24429  ustn0  24448  isphtpc  25223  tcphex  25446  tchnmfval  25457  bcthlem1  25553  bcthlem5  25557  dyadmbl  25829  itg2seq  25971  aannenlem3  26563  psercn  26659  abelth  26674  vmadivsum  27716  rpvmasumlem  27721  mudivsum  27764  selberglem1  27779  selberglem2  27780  selberg2lem  27784  selberg2  27785  pntrsumo1  27799  selbergr  27802  iscgrg  28852  isismt  28874  ishlg2  28942  ishlg  28945  ishpg  29114  iscgra  29193  isinag  29234  isleag  29243  wksv  30065  sspval  31190  ajfval  31276  shex  31679  chex  31693  hmopex  32342  ressplusf  33390  inftmrel  33607  isinftm  33608  esplymhp  34065  esplyfv1  34066  constrsuc  34235  dmvlsiga  34626  measbase  34695  ismeas  34697  isrnmeas  34698  faeval  34744  eulerpartlemmf  34873  eulerpartlemgvv  34874  signsplypnf  35045  signsply0  35046  afsval  35169  fineqvnttrclse  35637  kur14lem7  35778  kur14lem9  35780  satfvsuclem1  35925  fmlasuc0  35950  mppsval  36138  dfon2lem7  36353  colinearex  36627  poimirlem4  38360  heibor1lem  38546  rrnval  38564  lsatset  39850  lcvfbr  39880  cmtfvalN  40070  cvrfval  40128  lineset  40598  psubspset  40604  psubclsetN  40796  lautset  40942  pautsetN  40958  tendoset  41619  dicval  42036  ltex  43099  leex  43100  sn-isghm  43506  eldiophb  43589  pellexlem3  43659  pellexlem5  43661  onfrALTlem3VD  45696  modelaxreplem1  45788  rpex  46163  dmvolsal  47161  smfresal  47603  smfliminflem  47645  sectfn  49942  amgmlemALT  50808