Theorem ssexi 4803

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

Syntax hints:   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  zfausab  4811  ord3ex  4856  epse  5097  opabex  6483  fvclex  7138  oprabex  7156  tfrlem16  7489  oev  7594  sbthlem2  8071  phplem2  8140  php  8144  pssnn  8178  dffi3  8337  r0weon  8835  dfac3  8944  dfac5lem4  8949  dfac2  8953  hsmexlem6  9253  domtriomlem  9264  axdc3lem  9272  ac6  9302  brdom7disj  9353  brdom6disj  9354  konigthlem  9390  niex  9703  enqex  9744  npex  9808  enrex  9888  axcnex  9968  reex  10027  nnex  11026  zex  11386  qex  11800  ixxex  12186  ltweuz  12760  prmex  15391  1arithlem1  15627  1arith  15631  prdsval  16115  prdsle  16122  sectfval  16411  sscpwex  16475  issubc  16495  isfunc  16524  fullfunc  16566  fthfunc  16567  isfull  16570  isfth  16574  ipoval  17154  letsr  17227  nmznsg  17638  eqgfval  17642  isghm  17660  symgval  17799  ablfac1b  18469  lpival  19245  ltbval  19471  opsrle  19475  xrsle  19766  xrs10  19785  xrge0cmn  19788  znle  19884  cnmsgngrp  19925  psgninv  19928  cssval  20026  pjfval  20050  istopon  20717  dmtopon  20727  leordtval2  21016  lecldbas  21023  xkoopn  21392  xkouni  21402  xkoccn  21422  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  uzrest  21701  ustfn  22005  ustn0  22024  imasdsf1olem  22178  qtopbaslem  22562  isphtpc  22793  tchex  23016  tchnmfval  23027  bcthlem1  23121  bcthlem5  23125  dyadmbl  23368  itg2seq  23509  lhop1lem  23776  aannenlem3  24085  psercn  24180  abelth  24195  cxpcn2  24487  vmaval  24839  sqff1o  24908  musum  24917  vmadivsum  25171  rpvmasumlem  25176  mudivsum  25219  selberglem1  25234  selberglem2  25235  selberg2lem  25239  selberg2  25240  pntrsumo1  25254  selbergr  25257  iscgrg  25407  isismt  25429  ishlg  25497  ishpg  25651  iscgra  25701  isinag  25729  isleag  25733  pthsfval  26617  spthsfval  26618  crcts  26683  cycls  26684  eupths  27060  sspval  27578  ajfval  27664  shex  28069  chex  28083  hmopex  28734  ressplusf  29650  ressmulgnn  29683  inftmrel  29734  isinftm  29735  dmvlsiga  30192  measbase  30260  ismeas  30262  isrnmeas  30263  faeval  30309  eulerpartlemmf  30437  eulerpartlemgvv  30438  signsplypnf  30627  signsply0  30628  afsval  30749  kur14lem7  31194  kur14lem9  31196  mppsval  31469  dfon2lem7  31694  colinearex  32167  poimirlem4  33413  heibor1lem  33608  rrnval  33626  lsatset  34277  lcvfbr  34307  cmtfvalN  34497  cvrfval  34555  lineset  35024  psubspset  35030  psubclsetN  35222  lautset  35368  pautsetN  35384  tendoset  36047  dicval  36465  eldiophb  37320  pellexlem3  37395  pellexlem5  37397  onfrALTlem3VD  39123  dmvolsal  40564  smfresal  40995  smfliminflem  41036  amgmlemALT  42549