Theorem ssexi 5283

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  abex  5287  ord3ex  5348  epse  5632  opabex  7226  opabresex2  7474  mptexw  7965  fvclex  7971  oprabex  7988  mpoexw  8091  tfrlem16  8401  fosetex  8880  f1osetex  8881  dffi3  9423  r0weon  10091  dfac3  10200  dfac5lem4  10205  dfac2b  10209  hsmexlem6  10509  domtriomlem  10520  axdc3lem  10528  ac6  10558  brdom7disj  10610  brdom6disj  10611  niex  10966  enqex  11007  npex  11071  nrex1  11149  enrex  11152  reex  11291  nnex  12341  zex  12702  qex  13088  ixxex  13487  ltweuz  14104  seqexw  14160  cshwsexa  14975  prmex  16852  prdsval  17626  prdsle  17633  xrsle  17776  sectfval  17926  sscpwex  17990  issubc  18010  isfunc  18039  fullfunc  18083  fthfunc  18084  isfull  18087  isfth  18091  ipoval  18704  letsr  18767  ressmulgnn  19286  nmznsg  19378  eqgfval  19388  isghm  19430  lpival  21648  znle  21842  cssval  21988  pjfval  22012  ltbval  22352  opsrle  22356  istopon  23230  dmtopon  23241  leordtval2  23530  lecldbas  23537  xkoopn  23908  xkouni  23918  xkoccn  23938  xkoco1cn  23976  xkoco2cn  23977  xkococn  23979  xkoinjcn  24006  uzrest  24216  ustfn  24521  ustn0  24540  isphtpc  25315  tcphex  25538  tchnmfval  25549  bcthlem1  25645  bcthlem5  25649  dyadmbl  25921  itg2seq  26063  aannenlem3  26657  psercn  26753  abelth  26768  vmadivsum  27809  rpvmasumlem  27814  mudivsum  27857  selberglem1  27872  selberglem2  27873  selberg2lem  27877  selberg2  27878  pntrsumo1  27892  selbergr  27895  iscgrg  28975  isismt  28997  ishlg2  29065  ishlg  29068  ishpg  29237  iscgra  29316  isinag  29357  isleag  29366  wksv  30200  sspval  31325  ajfval  31411  shex  31814  chex  31828  hmopex  32477  ressplusf  33524  inftmrel  33741  isinftm  33742  esplymhp  34200  esplyfv1  34201  constrsuc  34370  dmvlsiga  34761  measbase  34830  ismeas  34832  isrnmeas  34833  faeval  34879  eulerpartlemmf  35007  eulerpartlemgvv  35008  signsplypnf  35179  signsply0  35180  afsval  35303  fineqvnttrclse  35792  kur14lem7  35977  kur14lem9  35979  satfvsuclem1  36124  fmlasuc0  36149  mppsval  36337  dfon2lem7  36551  colinearex  36825  poimirlem4  38543  heibor1lem  38744  rrnval  38762  lsatset  40048  lcvfbr  40078  cmtfvalN  40268  cvrfval  40326  lineset  40796  psubspset  40802  psubclsetN  40994  lautset  41140  pautsetN  41156  tendoset  41817  dicval  42234  ltex  43297  leex  43298  sn-isghm  43685  eldiophb  43768  pellexlem3  43838  pellexlem5  43840  onfrALTlem3VD  45869  modelaxreplem1  45968  rpex  46358  dmvolsal  47356  smfresal  47798  smfliminflem  47840  sectfn  50137  amgmlemALT  50988