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 2105  Vcvv 3492  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949
This theorem is referenced by:  zfausab  5224  ord3ex  5278  epse  5531  opabex  6974  mptexw  7643  fvclex  7649  oprabex  7666  mpoexw  7765  tfrlem16  8018  dffi3  8883  r0weon  9426  dfac3  9535  dfac5lem4  9540  dfac2b  9544  hsmexlem6  9841  domtriomlem  9852  axdc3lem  9860  ac6  9890  brdom7disj  9941  brdom6disj  9942  niex  10291  enqex  10332  npex  10396  nrex1  10474  enrex  10477  reex  10616  nnex  11632  zex  11978  qex  12348  ixxex  12737  ltweuz  13317  seqexw  13373  prmex  16009  prdsval  16716  prdsle  16723  sectfval  17009  sscpwex  17073  issubc  17093  isfunc  17122  fullfunc  17164  fthfunc  17165  isfull  17168  isfth  17172  ipoval  17752  letsr  17825  nmznsg  18258  eqgfval  18266  isghm  18296  symgval  18435  lpival  19946  ltbval  20180  opsrle  20184  xrsle  20493  znle  20611  cssval  20754  pjfval  20778  istopon  21448  dmtopon  21459  leordtval2  21748  lecldbas  21755  xkoopn  22125  xkouni  22135  xkoccn  22155  xkoco1cn  22193  xkoco2cn  22194  xkococn  22196  xkoinjcn  22223  uzrest  22433  ustfn  22737  ustn0  22756  isphtpc  23525  tcphex  23747  tchnmfval  23758  bcthlem1  23854  bcthlem5  23858  dyadmbl  24128  itg2seq  24270  aannenlem3  24846  psercn  24941  abelth  24956  vmadivsum  25985  rpvmasumlem  25990  mudivsum  26033  selberglem1  26048  selberglem2  26049  selberg2lem  26053  selberg2  26054  pntrsumo1  26068  selbergr  26071  iscgrg  26225  isismt  26247  ishlg  26315  ishpg  26472  iscgra  26522  isinag  26551  isleag  26560  pthsfval  27429  spthsfval  27430  crcts  27496  cycls  27497  eupths  27906  sspval  28427  ajfval  28513  shex  28916  chex  28930  hmopex  29579  ressplusf  30564  ressmulgnn  30597  inftmrel  30736  isinftm  30737  dmvlsiga  31287  measbase  31355  ismeas  31357  isrnmeas  31358  faeval  31404  eulerpartlemmf  31532  eulerpartlemgvv  31533  signsplypnf  31719  signsply0  31720  afsval  31841  kur14lem7  32356  kur14lem9  32358  satfvsuclem1  32503  fmlasuc0  32528  mppsval  32716  dfon2lem7  32931  colinearex  33418  poimirlem4  34777  heibor1lem  34968  rrnval  34986  lsatset  36006  lcvfbr  36036  cmtfvalN  36226  cvrfval  36284  lineset  36754  psubspset  36760  psubclsetN  36952  lautset  37098  pautsetN  37114  tendoset  37775  dicval  38192  eldiophb  39232  pellexlem3  39306  pellexlem5  39308  onfrALTlem3VD  41098  dmvolsal  42506  smfresal  42940  smfliminflem  42981  amgmlemALT  44832
  Copyright terms: Public domain W3C validator