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

Theorem ssexi 5005
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 5004 . 2 (𝐴𝐵𝐴 ∈ V)
41, 3ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  Vcvv 3398  wss 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783  df-ss 3790
This theorem is referenced by:  zfausab  5012  ord3ex  5063  epse  5301  opabex  6711  fvclex  7371  oprabex  7389  tfrlem16  7728  oev  7834  sbthlem2  8313  phplem2  8382  php  8386  pssnn  8420  dffi3  8579  r0weon  9121  dfac3  9230  dfac5lem4  9235  dfac2b  9239  dfac2OLD  9241  hsmexlem6  9541  domtriomlem  9552  axdc3lem  9560  ac6  9590  brdom7disj  9641  brdom6disj  9642  konigthlem  9678  niex  9991  enqex  10032  npex  10096  enrex  10176  axcnex  10256  reex  10315  nnex  11314  zex  11655  qex  12022  ixxex  12407  ltweuz  12987  prmex  15612  1arithlem1  15847  1arith  15851  prdsval  16323  prdsle  16330  sectfval  16618  sscpwex  16682  issubc  16702  isfunc  16731  fullfunc  16773  fthfunc  16774  isfull  16777  isfth  16781  ipoval  17362  letsr  17435  nmznsg  17843  eqgfval  17847  isghm  17865  symgval  18003  ablfac1b  18674  lpival  19457  ltbval  19683  opsrle  19687  xrsle  19977  xrs10  19996  xrge0cmn  19999  znle  20095  cnmsgngrp  20135  psgninv  20138  cssval  20240  pjfval  20264  istopon  20934  dmtopon  20945  leordtval2  21234  lecldbas  21241  xkoopn  21610  xkouni  21620  xkoccn  21640  xkoco1cn  21678  xkoco2cn  21679  xkococn  21681  xkoinjcn  21708  uzrest  21918  ustfn  22222  ustn0  22241  imasdsf1olem  22395  qtopbaslem  22779  isphtpc  23010  tchex  23232  tchnmfval  23243  bcthlem1  23338  bcthlem5  23342  dyadmbl  23587  itg2seq  23729  lhop1lem  23996  aannenlem3  24305  psercn  24400  abelth  24415  cxpcn2  24707  vmaval  25059  sqff1o  25128  musum  25137  vmadivsum  25391  rpvmasumlem  25396  mudivsum  25439  selberglem1  25454  selberglem2  25455  selberg2lem  25459  selberg2  25460  pntrsumo1  25474  selbergr  25477  iscgrg  25627  isismt  25649  ishlg  25717  ishpg  25871  iscgra  25921  isinag  25949  isleag  25953  pthsfval  26851  spthsfval  26852  crcts  26918  cycls  26919  eupths  27379  sspval  27912  ajfval  27998  shex  28403  chex  28417  hmopex  29068  ressplusf  29981  ressmulgnn  30014  inftmrel  30065  isinftm  30066  dmvlsiga  30523  measbase  30591  ismeas  30593  isrnmeas  30594  faeval  30640  eulerpartlemmf  30768  eulerpartlemgvv  30769  signsplypnf  30958  signsply0  30959  afsval  31080  kur14lem7  31522  kur14lem9  31524  mppsval  31797  dfon2lem7  32019  colinearex  32493  cnfinltrel  33559  poimirlem4  33728  heibor1lem  33921  rrnval  33939  lsatset  34772  lcvfbr  34802  cmtfvalN  34992  cvrfval  35050  lineset  35520  psubspset  35526  psubclsetN  35718  lautset  35864  pautsetN  35880  tendoset  36541  dicval  36958  eldiophb  37823  pellexlem3  37898  pellexlem5  37900  onfrALTlem3VD  39618  dmvolsal  41044  smfresal  41478  smfliminflem  41519  amgmlemALT  43121
  Copyright terms: Public domain W3C validator