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

Theorem ssexi 3706
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 3705 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1533  cvv 2500   wss 2810
This theorem is referenced by:  zfausab  3709  ord3ex  3744  moabex  3773  epse  3915  opabex  5130  fvclex  5208  abrexexlem1  5210  abrexex  5212  oprabex  5368  tfrlem16  5835  oev  5931  xpcomen  6337  sbthlem2  6356  phplem2  6472  php  6476  pssnn  6509  dffi3  6597  inf3lem3  6744  r0weon  7049  dfac3  7138  dfac5lem4  7143  dfac2a  7146  dfac2  7147  hsmexlem6  7426  domtriomlem  7436  axdc3lem  7444  brdom7disj  7537  brdom6disj  7538  unidom  7542  konigthlem  7565  niex  7829  enqex  7870  npex  7934  enrex  8016  axcnex  8093  reex  8151  nnex  8787  zex  9034  qex  9318  ixxex  9482  ltweuz  9755  1arithlem1  11168  1arith  11172  prdmlelem  11466  nmznsg  12040  eqgfval  12044  isghm  12055  symgval  12136  lpival  12969  ltbval  13180  opsrle  13183  znle  13399  cmpcld  13808  xkoopn  13963  xkouni  13969  xkoccn  13977  xkoco1cn  14007  xkoco2cn  14008  xkococn  14010  xkoinjcn  14037  hmph  14073  blfval  14268  qtopbaslem  14353  divcn  14416  evth  14449  isphtpc  14483  bcthlem1  14592  bcthlem5  14596  dyadmbl  14783  vitalilem2  14792  vitalilem3  14793  vitali  14796  itg2seq  14925  dvrec  15106  psercn  15517  abelth  15532  logcn  15683  sqff1o  16000  musum  16004  issubgoi  16311  sspval  16637  ajfval  16725  shex  17130  chex  17145  hmopex  17795  kur14lem7  18428  kur14lem9  18430  dfon2lem7  18829  colinearex  19376  prodex  19940  lteqttos  20311  issubcat  20550  isrocatset  20663  neibastop2lem1  20915  neibastop2lem4  20918  heibor1lem  21207  rngohomval  21271  istopon  21481  eldiophb  21581  pellexlem3  21689  pellexlem5  21691  setindtr  21894  aannenlem3  21985  onfrALTlem3VD  22757  bnj20  23129  bnj53  23908  lcvfbr  24348  cmtfval  24579  cvrfval  24637  lineset  25106  psubspset  25112  psubclset  25304  lautset  25450  pautset  25466  tendoset  26127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-v 2502  df-in 2817  df-ss 2821
Copyright terms: Public domain