Theorem ssexi 5288

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  abex  5292  ord3ex  5353  epse  5637  opabex  7246  opabresex2  7494  mptexw  7986  fvclex  7992  oprabex  8009  mpoexw  8113  tfrlem16  8426  fosetex  8905  f1osetex  8906  dffi3  9447  r0weon  10115  dfac3  10224  dfac5lem4  10229  dfac2b  10233  hsmexlem6  10533  domtriomlem  10544  axdc3lem  10552  brdom7disj  10634  brdom6disj  10635  niex  10990  enqex  11031  npex  11095  nrex1  11173  enrex  11176  reex  11315  nnex  12365  zex  12726  qex  13112  ixxex  13511  ltweuz  14128  seqexw  14184  cshwsexa  15000  prmex  16878  prdsval  17652  prdsle  17659  xrsle  17802  sectfval  17952  sscpwex  18016  issubc  18036  isfunc  18065  fullfunc  18109  fthfunc  18110  isfull  18113  isfth  18117  ipoval  18730  letsr  18793  ressmulgnn  19312  nmznsg  19404  eqgfval  19414  isghm  19456  lpival  21675  znle  21869  cssval  22015  pjfval  22039  ltbval  22379  opsrle  22383  istopon  23257  dmtopon  23268  leordtval2  23557  lecldbas  23564  xkoopn  23935  xkouni  23945  xkoccn  23965  xkoco1cn  24003  xkoco2cn  24004  xkococn  24006  xkoinjcn  24033  uzrest  24243  ustfn  24548  ustn0  24567  isphtpc  25342  tcphex  25565  tchnmfval  25576  bcthlem1  25672  bcthlem5  25676  dyadmbl  25948  itg2seq  26090  aannenlem3  26684  psercn  26780  abelth  26795  vmadivsum  27836  rpvmasumlem  27841  mudivsum  27884  selberglem1  27899  selberglem2  27900  selberg2lem  27904  selberg2  27905  pntrsumo1  27919  selbergr  27922  iscgrg  29002  isismt  29024  ishlg2  29092  ishlg  29095  ishpg  29264  iscgra  29343  isinag  29384  isleag  29393  wksv  30227  sspval  31352  ajfval  31438  shex  31841  chex  31855  hmopex  32504  ressplusf  33591  inftmrel  33808  isinftm  33809  esplymhp  34267  esplyfv1  34268  constrsuc  34437  dmvlsiga  34828  measbase  34897  ismeas  34899  isrnmeas  34900  faeval  34946  eulerpartlemmf  35074  eulerpartlemgvv  35075  signsplypnf  35246  signsply0  35247  afsval  35370  rankse  35822  fineqvnttrclse  35891  kur14lem7  36143  kur14lem9  36145  satfvsuclem1  36290  fmlasuc0  36315  mppsval  36503  dfon2lem7  36728  colinearex  37002  poimirlem4  38733  heibor1lem  38934  rrnval  38952  lsatset  40238  lcvfbr  40268  cmtfvalN  40458  cvrfval  40516  lineset  40986  psubspset  40992  psubclsetN  41184  lautset  41330  pautsetN  41346  tendoset  42007  dicval  42424  ltex  43487  leex  43488  sn-isghm  43875  eldiophb  43959  pellexlem3  44029  pellexlem5  44031  onfrALTlem3VD  46058  modelaxreplem1  46161  rpex  46561  dmvolsal  47559  smfresal  48001  smfliminflem  48043  sectfn  50346  parcatid  50967  amgmlemALT  51266