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

Theorem ssexi 4801
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 4800 . 2 (𝐴𝐵𝐴 ∈ V)
41, 3ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  Vcvv 3198  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586
This theorem is referenced by:  zfausab  4809  ord3ex  4854  epse  5095  opabex  6480  fvclex  7135  oprabex  7153  tfrlem16  7486  oev  7591  sbthlem2  8068  phplem2  8137  php  8141  pssnn  8175  dffi3  8334  r0weon  8832  dfac3  8941  dfac5lem4  8946  dfac2  8950  hsmexlem6  9250  domtriomlem  9261  axdc3lem  9269  ac6  9299  brdom7disj  9350  brdom6disj  9351  konigthlem  9387  niex  9700  enqex  9741  npex  9805  enrex  9885  axcnex  9965  reex  10024  nnex  11023  zex  11383  qex  11797  ixxex  12183  ltweuz  12755  prmex  15385  1arithlem1  15621  1arith  15625  prdsval  16109  prdsle  16116  sectfval  16405  sscpwex  16469  issubc  16489  isfunc  16518  fullfunc  16560  fthfunc  16561  isfull  16564  isfth  16568  ipoval  17148  letsr  17221  nmznsg  17632  eqgfval  17636  isghm  17654  symgval  17793  ablfac1b  18463  lpival  19239  ltbval  19465  opsrle  19469  xrsle  19760  xrs10  19779  xrge0cmn  19782  znle  19878  cnmsgngrp  19919  psgninv  19922  cssval  20020  pjfval  20044  istopon  20711  dmtopon  20721  leordtval2  21010  lecldbas  21017  xkoopn  21386  xkouni  21396  xkoccn  21416  xkoco1cn  21454  xkoco2cn  21455  xkococn  21457  xkoinjcn  21484  uzrest  21695  ustfn  21999  ustn0  22018  imasdsf1olem  22172  qtopbaslem  22556  isphtpc  22787  tchex  23010  tchnmfval  23021  bcthlem1  23115  bcthlem5  23119  dyadmbl  23362  itg2seq  23503  lhop1lem  23770  aannenlem3  24079  psercn  24174  abelth  24189  cxpcn2  24481  vmaval  24833  sqff1o  24902  musum  24911  vmadivsum  25165  rpvmasumlem  25170  mudivsum  25213  selberglem1  25228  selberglem2  25229  selberg2lem  25233  selberg2  25234  pntrsumo1  25248  selbergr  25251  iscgrg  25401  isismt  25423  ishlg  25491  ishpg  25645  iscgra  25695  isinag  25723  isleag  25727  pthsfval  26611  spthsfval  26612  crcts  26677  cycls  26678  eupths  27053  sspval  27562  ajfval  27648  shex  28053  chex  28067  hmopex  28718  ressplusf  29635  ressmulgnn  29668  inftmrel  29719  isinftm  29720  dmvlsiga  30177  measbase  30245  ismeas  30247  isrnmeas  30248  faeval  30294  eulerpartlemmf  30422  eulerpartlemgvv  30423  signsplypnf  30612  signsply0  30613  afsval  30734  kur14lem7  31179  kur14lem9  31181  mppsval  31454  dfon2lem7  31678  colinearex  32151  poimirlem4  33393  heibor1lem  33588  rrnval  33606  lsatset  34103  lcvfbr  34133  cmtfvalN  34323  cvrfval  34381  lineset  34850  psubspset  34856  psubclsetN  35048  lautset  35194  pautsetN  35210  tendoset  35873  dicval  36291  eldiophb  37146  pellexlem3  37221  pellexlem5  37223  onfrALTlem3VD  38949  dmvolsal  40333  smfresal  40764  smfliminflem  40805  amgmlemALT  42320
  Copyright terms: Public domain W3C validator