Theorem ssexi 5284

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899

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 2732  ax-sep 5249

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  abex  5288  ord3ex  5349  epse  5630  opabex  7215  opabresex2  7463  mptexw  7949  fvclex  7955  oprabex  7972  mpoexw  8075  tfrlem16  8380  fosetex  8859  f1osetex  8860  dffi3  9401  r0weon  10048  dfac3  10157  dfac5lem4  10162  dfac2b  10166  hsmexlem6  10466  domtriomlem  10477  axdc3lem  10485  ac6  10515  brdom7disj  10567  brdom6disj  10568  niex  10923  enqex  10964  npex  11028  nrex1  11106  enrex  11109  reex  11248  nnex  12296  zex  12657  qex  13043  ixxex  13442  ltweuz  14058  seqexw  14114  cshwsexa  14928  prmex  16800  prdsval  17573  prdsle  17580  xrsle  17723  sectfval  17873  sscpwex  17937  issubc  17957  isfunc  17986  fullfunc  18030  fthfunc  18031  isfull  18034  isfth  18038  ipoval  18651  letsr  18714  ressmulgnn  19233  nmznsg  19325  eqgfval  19335  isghm  19377  lpival  21595  znle  21789  cssval  21935  pjfval  21959  ltbval  22299  opsrle  22303  istopon  23177  dmtopon  23188  leordtval2  23477  lecldbas  23484  xkoopn  23855  xkouni  23865  xkoccn  23885  xkoco1cn  23923  xkoco2cn  23924  xkococn  23926  xkoinjcn  23953  uzrest  24163  ustfn  24468  ustn0  24487  isphtpc  25262  tcphex  25485  tchnmfval  25496  bcthlem1  25592  bcthlem5  25596  dyadmbl  25868  itg2seq  26010  aannenlem3  26606  psercn  26702  abelth  26717  vmadivsum  27758  rpvmasumlem  27763  mudivsum  27806  selberglem1  27821  selberglem2  27822  selberg2lem  27826  selberg2  27827  pntrsumo1  27841  selbergr  27844  iscgrg  28894  isismt  28916  ishlg2  28984  ishlg  28987  ishpg  29156  iscgra  29235  isinag  29276  isleag  29285  wksv  30119  sspval  31244  ajfval  31330  shex  31733  chex  31747  hmopex  32396  ressplusf  33443  inftmrel  33660  isinftm  33661  esplymhp  34119  esplyfv1  34120  constrsuc  34289  dmvlsiga  34680  measbase  34749  ismeas  34751  isrnmeas  34752  faeval  34798  eulerpartlemmf  34927  eulerpartlemgvv  34928  signsplypnf  35099  signsply0  35100  afsval  35223  fineqvnttrclse  35711  kur14lem7  35892  kur14lem9  35894  satfvsuclem1  36039  fmlasuc0  36064  mppsval  36252  dfon2lem7  36467  colinearex  36741  poimirlem4  38456  heibor1lem  38657  rrnval  38675  lsatset  39961  lcvfbr  39991  cmtfvalN  40181  cvrfval  40239  lineset  40709  psubspset  40715  psubclsetN  40907  lautset  41053  pautsetN  41069  tendoset  41730  dicval  42147  ltex  43210  leex  43211  sn-isghm  43617  eldiophb  43700  pellexlem3  43770  pellexlem5  43772  onfrALTlem3VD  45807  modelaxreplem1  45899  rpex  46274  dmvolsal  47272  smfresal  47714  smfliminflem  47756  sectfn  50053  amgmlemALT  50904