Theorem ssexi 5246

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  zfausab  5254  ord3ex  5310  epse  5572  opabex  7096  opabresex2  7327  mptexw  7795  fvclex  7801  oprabex  7819  mpoexw  7919  tfrlem16  8224  fosetex  8646  f1osetex  8647  dffi3  9190  r0weon  9768  dfac3  9877  dfac5lem4  9882  dfac2b  9886  hsmexlem6  10187  domtriomlem  10198  axdc3lem  10206  ac6  10236  brdom7disj  10287  brdom6disj  10288  niex  10637  enqex  10678  npex  10742  nrex1  10820  enrex  10823  reex  10962  nnex  11979  zex  12328  qex  12701  ixxex  13090  ltweuz  13681  seqexw  13737  prmex  16382  prdsval  17166  prdsle  17173  sectfval  17463  sscpwex  17527  issubc  17550  isfunc  17579  fullfunc  17622  fthfunc  17623  isfull  17626  isfth  17630  ipoval  18248  letsr  18311  nmznsg  18796  eqgfval  18804  isghm  18834  lpival  20516  xrsle  20618  znle  20740  cssval  20887  pjfval  20913  ltbval  21244  opsrle  21248  istopon  22061  dmtopon  22072  leordtval2  22363  lecldbas  22370  xkoopn  22740  xkouni  22750  xkoccn  22770  xkoco1cn  22808  xkoco2cn  22809  xkococn  22811  xkoinjcn  22838  uzrest  23048  ustfn  23353  ustn0  23372  isphtpc  24157  tcphex  24381  tchnmfval  24392  bcthlem1  24488  bcthlem5  24492  dyadmbl  24764  itg2seq  24907  aannenlem3  25490  psercn  25585  abelth  25600  vmadivsum  26630  rpvmasumlem  26635  mudivsum  26678  selberglem1  26693  selberglem2  26694  selberg2lem  26698  selberg2  26699  pntrsumo1  26713  selbergr  26716  iscgrg  26873  isismt  26895  ishlg  26963  ishpg  27120  iscgra  27170  isinag  27199  isleag  27208  wksv  27986  sspval  29085  ajfval  29171  shex  29574  chex  29588  hmopex  30237  ressplusf  31235  ressmulgnn  31292  inftmrel  31434  isinftm  31435  dmvlsiga  32097  measbase  32165  ismeas  32167  isrnmeas  32168  faeval  32214  eulerpartlemmf  32342  eulerpartlemgvv  32343  signsplypnf  32529  signsply0  32530  afsval  32651  kur14lem7  33174  kur14lem9  33176  satfvsuclem1  33321  fmlasuc0  33346  mppsval  33534  dfon2lem7  33765  colinearex  34362  poimirlem4  35781  heibor1lem  35967  rrnval  35985  lsatset  37004  lcvfbr  37034  cmtfvalN  37224  cvrfval  37282  lineset  37752  psubspset  37758  psubclsetN  37950  lautset  38096  pautsetN  38112  tendoset  38773  dicval  39190  eldiophb  40579  pellexlem3  40653  pellexlem5  40655  onfrALTlem3VD  42507  dmvolsal  43885  smfresal  44322  smfliminflem  44363  amgmlemALT  46507  upwordsseti  46520