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

Theorem ssexi 3474
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 3473 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1427  cvv 2335   wss 2635
This theorem is referenced by:  zfausab 3477  ord3ex 3512  moabex 3541  opabex 4798  fvclex 4865  abrexexlem1 4867  abrexex 4869  oprabex 4996  oev 5426  sbthlem2 5776  phplem2 5892  phplem4 5894  php 5896  pssnn 5931  ordtypelem1 6033  hartogslem 6041  inf3lem3 6072  hta 6242  aceq3 6327  aceq5lem4 6332  aceq6b 6336  domtriomlem 6444  axdc3lem 6451  axcclem 6458  zorn2lem1 6508  brdom7disj 6528  brdom6disj 6529  unidom 6532  konigthlem 6558  infmap2lem2 6579  gch-kn 6586  niex 6776  enqex 6818  npex 6882  enrex 6965  1arithlem1 9885  1arith 9889  strss 10029  issubgoi 10897  symgval 11003  cmpcld 11344  hmph 11413  blfval 11532  qtopbaslem 11614  divcn 11664  evth 11696  phtpyfval 11701  phtpcval 11708  pi1bval 11736  bcthlem1 11812  bcthlem5 11816  sspval 12021  ajfval 12109  vitalilem2 12368  vitalilem3 12369  vitali 12372  itg2seq 12501  shex 13446  chex 13461  hmopex 14111  dfon2lem7 15027  colinearex 15584  issubcat 16862  isrocatset 16975  2ndcctbss 17212  neibastop2lem1 17253  neibastop2lem4 17256  heibor1lem 17573  heiborlem3 17577  rngohomval 17637  eldiophb 17856  pellexlem4 17973  pellexlem5 17974  pellex 17976  setindtr 18178  onfrALTlem3VD 19041  bnj20 19406  bnj53 20185  cmtfval 20771  cvrfval 20829  lineset 21316  psubspset 21322  psubclset 21515  lautset 21664  pautset 21685  tendoset 22439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-sep 3455
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-v 2337  df-in 2642  df-ss 2644
Copyright terms: Public domain