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

Theorem ssexi 4723
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 4722 . 2 (𝐴𝐵𝐴 ∈ V)
41, 3ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3169  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550
This theorem is referenced by:  zfausab  4730  ord3ex  4774  epse  5008  opabex  6363  fvclex  7005  oprabex  7021  tfrlem16  7350  oev  7455  sbthlem2  7930  phplem2  7999  php  8003  pssnn  8037  dffi3  8194  r0weon  8692  dfac3  8801  dfac5lem4  8806  dfac2  8810  hsmexlem6  9110  domtriomlem  9121  axdc3lem  9129  ac6  9159  brdom7disj  9208  brdom6disj  9209  konigthlem  9243  niex  9556  enqex  9597  npex  9661  enrex  9741  axcnex  9821  reex  9880  nnex  10870  zex  11216  qex  11629  ixxex  12010  ltweuz  12574  prmex  15172  1arithlem1  15408  1arith  15412  prdsval  15881  prdsle  15888  sectfval  16177  sscpwex  16241  issubc  16261  isfunc  16290  fullfunc  16332  fthfunc  16333  isfull  16336  isfth  16340  ipoval  16920  letsr  16993  nmznsg  17404  eqgfval  17408  isghm  17426  symgval  17565  ablfac1b  18235  lpival  19009  ltbval  19235  opsrle  19239  xrsle  19528  xrs10  19547  xrge0cmn  19550  znle  19645  cnmsgngrp  19686  psgninv  19689  cssval  19784  pjfval  19808  istopon  20479  leordtval2  20765  lecldbas  20772  xkoopn  21141  xkouni  21151  xkoccn  21171  xkoco1cn  21209  xkoco2cn  21210  xkococn  21212  xkoinjcn  21239  uzrest  21450  ustfn  21754  ustn0  21773  imasdsf1olem  21926  qtopbaslem  22301  isphtpc  22529  tchex  22742  tchnmfval  22753  bcthlem1  22843  bcthlem5  22847  dyadmbl  23088  itg2seq  23229  lhop1lem  23494  aannenlem3  23803  psercn  23898  abelth  23913  cxpcn2  24201  vmaval  24553  sqff1o  24622  musum  24631  vmadivsum  24885  rpvmasumlem  24890  mudivsum  24933  selberglem1  24948  selberglem2  24949  selberg2lem  24953  selberg2  24954  pntrsumo1  24968  selbergr  24971  iscgrg  25122  isismt  25144  ishlg  25212  ishpg  25366  iscgra  25416  isinag  25444  isleag  25448  sspval  26763  ajfval  26851  shex  27256  chex  27270  hmopex  27921  ressplusf  28784  ressmulgnn  28817  inftmrel  28868  isinftm  28869  dmvlsiga  29322  measbase  29390  ismeas  29392  isrnmeas  29393  faeval  29439  eulerpartlemmf  29567  eulerpartlemgvv  29568  signsplypnf  29756  signsply0  29757  afsval  29805  kur14lem7  30251  kur14lem9  30253  mppsval  30526  dfon2lem7  30741  colinearex  31140  bj-dmtopon  32042  poimirlem4  32383  heibor1lem  32578  rrnval  32596  lsatset  33095  lcvfbr  33125  cmtfvalN  33315  cvrfval  33373  lineset  33842  psubspset  33848  psubclsetN  34040  lautset  34186  pautsetN  34202  tendoset  34865  dicval  35283  eldiophb  36138  pellexlem3  36213  pellexlem5  36215  onfrALTlem3VD  37945  dmvolsal  39041  smfresal  39474  pthsfval  40926  spthsfval  40927  crctS  40993  cyclS  40994  eupths  41366  amgmlemALT  42318
  Copyright terms: Public domain W3C validator