Theorem ssexi 5241

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  zfausab  5249  ord3ex  5305  epse  5563  opabex  7078  mptexw  7769  fvclex  7775  oprabex  7792  mpoexw  7892  tfrlem16  8195  fosetex  8604  f1osetex  8605  dffi3  9120  r0weon  9699  dfac3  9808  dfac5lem4  9813  dfac2b  9817  hsmexlem6  10118  domtriomlem  10129  axdc3lem  10137  ac6  10167  brdom7disj  10218  brdom6disj  10219  niex  10568  enqex  10609  npex  10673  nrex1  10751  enrex  10754  reex  10893  nnex  11909  zex  12258  qex  12630  ixxex  13019  ltweuz  13609  seqexw  13665  prmex  16310  prdsval  17083  prdsle  17090  sectfval  17380  sscpwex  17444  issubc  17466  isfunc  17495  fullfunc  17538  fthfunc  17539  isfull  17542  isfth  17546  ipoval  18163  letsr  18226  nmznsg  18711  eqgfval  18719  isghm  18749  lpival  20429  xrsle  20530  znle  20652  cssval  20799  pjfval  20823  ltbval  21154  opsrle  21158  istopon  21969  dmtopon  21980  leordtval2  22271  lecldbas  22278  xkoopn  22648  xkouni  22658  xkoccn  22678  xkoco1cn  22716  xkoco2cn  22717  xkococn  22719  xkoinjcn  22746  uzrest  22956  ustfn  23261  ustn0  23280  isphtpc  24063  tcphex  24286  tchnmfval  24297  bcthlem1  24393  bcthlem5  24397  dyadmbl  24669  itg2seq  24812  aannenlem3  25395  psercn  25490  abelth  25505  vmadivsum  26535  rpvmasumlem  26540  mudivsum  26583  selberglem1  26598  selberglem2  26599  selberg2lem  26603  selberg2  26604  pntrsumo1  26618  selbergr  26621  iscgrg  26777  isismt  26799  ishlg  26867  ishpg  27024  iscgra  27074  isinag  27103  isleag  27112  pthsfval  27990  spthsfval  27991  crcts  28057  cycls  28058  eupths  28465  sspval  28986  ajfval  29072  shex  29475  chex  29489  hmopex  30138  ressplusf  31137  ressmulgnn  31194  inftmrel  31336  isinftm  31337  dmvlsiga  31997  measbase  32065  ismeas  32067  isrnmeas  32068  faeval  32114  eulerpartlemmf  32242  eulerpartlemgvv  32243  signsplypnf  32429  signsply0  32430  afsval  32551  kur14lem7  33074  kur14lem9  33076  satfvsuclem1  33221  fmlasuc0  33246  mppsval  33434  dfon2lem7  33671  colinearex  34289  poimirlem4  35708  heibor1lem  35894  rrnval  35912  lsatset  36931  lcvfbr  36961  cmtfvalN  37151  cvrfval  37209  lineset  37679  psubspset  37685  psubclsetN  37877  lautset  38023  pautsetN  38039  tendoset  38700  dicval  39117  eldiophb  40495  pellexlem3  40569  pellexlem5  40571  onfrALTlem3VD  42396  dmvolsal  43775  smfresal  44209  smfliminflem  44250  amgmlemALT  46393