HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexi 3645
Description: The subset of a set is also a set.
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 3644 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1528  cvv 2440   wss 2750
This theorem is referenced by:  zfausab 3648  ord3ex 3683  moabex 3712  opabex 5048  fvclex 5125  abrexexlem1 5127  abrexex 5129  oprabex 5278  oev 5826  sbthlem2 6222  phplem2 6342  php 6346  pssnn 6379  ordtypelem1 6512  inf3lem3 6597  hta 6820  dfac3 6979  dfac5lem4 6984  dfac2 6988  hsmexlem6 7271  domtriomlem 7281  axdc3lem 7289  brdom7disj 7382  brdom6disj 7383  unidom 7387  konigthlem 7410  niex 7674  enqex 7716  npex 7780  enrex 7863  1arithlem1 10988  1arith 10992  prdmlelem 11281  nmznsg 11852  eqgfval 11856  isghm 11867  symgval 11948  lpival 12757  ltbval 12951  opsrle 12954  znle 13152  cmpcld 13559  xkoopn 13713  xkouni 13719  xkoccn 13727  xkoco1cn 13757  xkoco2cn 13758  xkococn 13760  xkoinjcn 13787  hmph 13823  blfval 14014  qtopbaslem 14099  divcn 14162  evth 14195  isphtpc 14229  pi1bval 14266  bcthlem1 14327  bcthlem5 14331  dyadmbl 14518  vitalilem2 14527  vitalilem3 14528  vitali 14531  itg2seq 14660  dvrec 14841  psercn 15244  abelth 15259  logcn 15410  issubgoi 16023  sspval 16349  ajfval 16437  shex 16842  chex 16857  hmopex 17507  kur14lem7 18140  kur14lem9 18142  dfon2lem7 18524  colinearex 19081  prodex 19646  lteqttos 20017  issubcat 20256  isrocatset 20369  neibastop2lem1 20621  neibastop2lem4 20624  heibor1lem 20915  rngohomval 20979  istopon 21189  eldiophb 21289  pellexlem3 21397  pellexlem5 21399  setindtr 21602  aannenlem3 21699  onfrALTlem3VD 22457  bnj20 22829  bnj53 23608  lcvfbr 24048  cmtfval 24279  cvrfval 24337  lineset 24806  psubspset 24812  psubclset 25004  lautset 25150  pautset 25166  tendoset 25827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-v 2442  df-in 2757  df-ss 2761
Copyright terms: Public domain