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

Theorem ssexi 4597
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
Hypotheses
Ref Expression
ssexi.1
ssexi.2
Assertion
Ref Expression
ssexi

Proof of Theorem ssexi
StepHypRef Expression
1 ssexi.2 . 2
2 ssexi.1 . . 3
32ssex 4596 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  C_wss 3475
This theorem is referenced by:  zfausab  4601  ord3ex  4642  epse  4867  opabex  6141  fvclex  6772  oprabex  6788  tfrlem16  7081  oev  7183  sbthlem2  7648  phplem2  7717  php  7721  pssnn  7758  dffi3  7911  inf3lem3  8068  r0weon  8411  dfac3  8523  dfac5lem4  8528  dfac2  8532  hsmexlem6  8832  domtriomlem  8843  axdc3lem  8851  ac6  8881  brdom7disj  8930  brdom6disj  8931  konigthlem  8964  niex  9280  enqex  9321  npex  9385  enrex  9465  axcnex  9545  reex  9604  nnex  10567  zex  10898  qex  11223  ixxex  11569  ltweuz  12072  1arithlem1  14441  1arith  14445  prdsval  14852  prdsle  14859  sectfval  15146  sscpwex  15184  issubc  15204  isfunc  15233  fullfunc  15275  fthfunc  15276  isfull  15279  isfth  15283  ipoval  15784  letsr  15857  nmznsg  16245  eqgfval  16249  isghm  16267  symgval  16404  ablfac1b  17121  lpival  17893  ltbval  18136  opsrle  18140  xrsle  18438  xrs10  18457  xrge0cmn  18460  znle  18573  cnmsgngrp  18615  psgninv  18618  cssval  18713  pjfval  18737  istopon  19426  leordtval2  19713  lecldbas  19720  xkoopn  20090  xkouni  20100  xkoccn  20120  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  uzrest  20398  ustfn  20704  ustn0  20723  imasdsf1olem  20876  qtopbaslem  21265  isphtpc  21494  tchex  21660  tchnmfval  21671  bcthlem1  21763  bcthlem5  21767  dyadmbl  22009  itg2seq  22149  lhop1lem  22414  aannenlem3  22726  psercn  22821  abelth  22836  cxpcn2  23120  vmaval  23387  sqff1o  23456  musum  23467  vmadivsum  23667  rpvmasumlem  23672  mudivsum  23715  selberglem1  23730  selberglem2  23731  selberg2lem  23735  selberg2  23736  pntrsumo1  23750  selbergr  23753  iscgrg  23904  isismt  23921  ishlg  23986  ishpg  24128  iscgra  24169  issubgoi  25312  sspval  25636  ajfval  25724  shex  26129  chex  26144  hmopex  26794  ressplusf  27638  ressmulgnn  27671  inftmrel  27724  isinftm  27725  dmvlsiga  28129  measbase  28168  ismeas  28170  isrnmeas  28171  faeval  28218  eulerpartlemmf  28314  eulerpartlemgvv  28315  signsplypnf  28507  signsply0  28508  afsval  28551  kur14lem7  28656  kur14lem9  28658  mppsval  28932  dfon2lem7  29221  colinearex  29710  heibor1lem  30305  rrnval  30323  eldiophb  30690  pellexlem3  30767  pellexlem5  30769  setindtr  30966  onfrALTlem3VD  33687  lsatset  34715  lcvfbr  34745  cmtfvalN  34935  cvrfval  34993  lineset  35462  psubspset  35468  psubclsetN  35660  lautset  35806  pautsetN  35822  tendoset  36485  dicval  36903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator