Theorem ssexi 5253

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

Syntax hints:   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902

This theorem is referenced by:  abex  5257  zfausab  5263  ord3ex  5319  epse  5603  opabex  7168  opabresex2  7414  mptexw  7899  fvclex  7905  oprabex  7922  mpoexw  8024  tfrlem16  8326  fosetex  8799  f1osetex  8800  dffi3  9338  r0weon  9929  dfac3  10038  dfac5lem4  10043  dfac5lem4OLD  10045  dfac2b  10048  hsmexlem6  10348  domtriomlem  10359  axdc3lem  10367  ac6  10397  brdom7disj  10448  brdom6disj  10449  niex  10799  enqex  10840  npex  10904  nrex1  10982  enrex  10985  reex  11124  nnex  12175  zex  12528  qex  12906  ixxex  13304  ltweuz  13918  seqexw  13974  cshwsexa  14781  prmex  16641  prdsval  17413  prdsle  17420  xrsle  17563  sectfval  17713  sscpwex  17777  issubc  17797  isfunc  17826  fullfunc  17870  fthfunc  17871  isfull  17874  isfth  17878  ipoval  18491  letsr  18554  ressmulgnn  19047  nmznsg  19138  eqgfval  19146  isghm  19185  isghmOLD  19186  lpival  21321  znle  21515  cssval  21661  pjfval  21685  ltbval  22023  opsrle  22027  istopon  22899  dmtopon  22910  leordtval2  23199  lecldbas  23206  xkoopn  23576  xkouni  23586  xkoccn  23606  xkoco1cn  23644  xkoco2cn  23645  xkococn  23647  xkoinjcn  23674  uzrest  23884  ustfn  24189  ustn0  24208  isphtpc  24983  tcphex  25206  tchnmfval  25217  bcthlem1  25313  bcthlem5  25317  dyadmbl  25589  itg2seq  25731  aannenlem3  26318  psercn  26413  abelth  26428  vmadivsum  27467  rpvmasumlem  27472  mudivsum  27515  selberglem1  27530  selberglem2  27531  selberg2lem  27535  selberg2  27536  pntrsumo1  27550  selbergr  27553  iscgrg  28602  isismt  28624  ishlg  28692  ishpg  28849  iscgra  28899  isinag  28928  isleag  28937  wksv  29710  sspval  30816  ajfval  30902  shex  31305  chex  31319  hmopex  31968  ressplusf  33046  inftmrel  33265  isinftm  33266  esplymhp  33764  esplyfv1  33765  constrsuc  33934  dmvlsiga  34325  measbase  34393  ismeas  34395  isrnmeas  34396  faeval  34442  eulerpartlemmf  34571  eulerpartlemgvv  34572  signsplypnf  34746  signsply0  34747  afsval  34870  fineqvnttrclse  35320  kur14lem7  35455  kur14lem9  35457  satfvsuclem1  35602  fmlasuc0  35627  mppsval  35815  dfon2lem7  36030  colinearex  36303  poimirlem4  38006  heibor1lem  38191  rrnval  38209  lsatset  39497  lcvfbr  39527  cmtfvalN  39717  cvrfval  39775  lineset  40245  psubspset  40251  psubclsetN  40443  lautset  40589  pautsetN  40605  tendoset  41266  dicval  41683  ltex  42744  leex  42745  sn-isghm  43138  eldiophb  43221  pellexlem3  43291  pellexlem5  43293  onfrALTlem3VD  45345  modelaxreplem1  45437  rpex  45805  dmvolsal  46803  smfresal  47245  smfliminflem  47287  sectfn  49533  amgmlemALT  50307