MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexi Structured version   Visualization version   GIF version

Theorem ssexi 5217
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
StepHypRef Expression
1 ssexi.2 . 2 𝐴𝐵
2 ssexi.1 . . 3 𝐵 ∈ V
32ssex 5216 . 2 (𝐴𝐵𝐴 ∈ V)
41, 3ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3493  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-in 3941  df-ss 3950
This theorem is referenced by:  zfausab  5224  ord3ex  5278  epse  5531  opabex  6975  mptexw  7646  fvclex  7652  oprabex  7669  mpoexw  7768  tfrlem16  8021  dffi3  8887  r0weon  9430  dfac3  9539  dfac5lem4  9544  dfac2b  9548  hsmexlem6  9845  domtriomlem  9856  axdc3lem  9864  ac6  9894  brdom7disj  9945  brdom6disj  9946  niex  10295  enqex  10336  npex  10400  nrex1  10478  enrex  10481  reex  10620  nnex  11636  zex  11982  qex  12352  ixxex  12741  ltweuz  13321  seqexw  13377  prmex  16013  prdsval  16720  prdsle  16727  sectfval  17013  sscpwex  17077  issubc  17097  isfunc  17126  fullfunc  17168  fthfunc  17169  isfull  17172  isfth  17176  ipoval  17756  letsr  17829  nmznsg  18312  eqgfval  18320  isghm  18350  lpival  20010  ltbval  20244  opsrle  20248  xrsle  20557  znle  20675  cssval  20818  pjfval  20842  istopon  21512  dmtopon  21523  leordtval2  21812  lecldbas  21819  xkoopn  22189  xkouni  22199  xkoccn  22219  xkoco1cn  22257  xkoco2cn  22258  xkococn  22260  xkoinjcn  22287  uzrest  22497  ustfn  22802  ustn0  22821  isphtpc  23590  tcphex  23812  tchnmfval  23823  bcthlem1  23919  bcthlem5  23923  dyadmbl  24193  itg2seq  24335  aannenlem3  24911  psercn  25006  abelth  25021  vmadivsum  26050  rpvmasumlem  26055  mudivsum  26098  selberglem1  26113  selberglem2  26114  selberg2lem  26118  selberg2  26119  pntrsumo1  26133  selbergr  26136  iscgrg  26290  isismt  26312  ishlg  26380  ishpg  26537  iscgra  26587  isinag  26616  isleag  26625  pthsfval  27494  spthsfval  27495  crcts  27561  cycls  27562  eupths  27971  sspval  28492  ajfval  28578  shex  28981  chex  28995  hmopex  29644  ressplusf  30630  ressmulgnn  30663  inftmrel  30802  isinftm  30803  dmvlsiga  31381  measbase  31449  ismeas  31451  isrnmeas  31452  faeval  31498  eulerpartlemmf  31626  eulerpartlemgvv  31627  signsplypnf  31813  signsply0  31814  afsval  31935  kur14lem7  32452  kur14lem9  32454  satfvsuclem1  32599  fmlasuc0  32624  mppsval  32812  dfon2lem7  33027  colinearex  33514  poimirlem4  34888  heibor1lem  35079  rrnval  35097  lsatset  36118  lcvfbr  36148  cmtfvalN  36338  cvrfval  36396  lineset  36866  psubspset  36872  psubclsetN  37064  lautset  37210  pautsetN  37226  tendoset  37887  dicval  38304  eldiophb  39344  pellexlem3  39418  pellexlem5  39420  onfrALTlem3VD  41211  dmvolsal  42619  smfresal  43053  smfliminflem  43094  amgmlemALT  44894
  Copyright terms: Public domain W3C validator