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

Theorem ssexi 3510
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 3509 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1416  cvv 2327   wss 2637
This theorem is referenced by:  zfausab 3513  ord3ex 3548  moabex 3577  opabex 4889  fvclex 4964  abrexexlem1 4966  abrexex 4968  oprabex 5103  oev 5595  sbthlem2 5965  phplem2 6081  php 6085  pssnn 6117  ordtypelem1 6233  hartogslem 6241  inf3lem3 6279  hta 6451  aceq3 6546  aceq5lem4 6551  aceq6b 6555  domtriomlem 6706  axdc3lem 6713  zorn2lem1 6771  brdom7disj 6791  brdom6disj 6792  unidom 6795  konigthlem 6820  niex 7023  enqex 7065  npex 7129  enrex 7212  1arithlem1 10324  1arith 10328  prdmlelem 10615  nmznsg 11108  eqgfval 11111  isghm 11120  symgval 11179  issubgoi 11891  cmpcld 12371  xkoopn 12525  xkouni 12531  xkoccn 12539  xkoco1cn 12569  xkoco2cn 12570  xkococn 12572  xkoinjcn 12599  hmph 12634  blfval 12797  qtopbaslem 12882  divcn 12945  evth 12978  isphtpc 13012  pi1bval 13049  bcthlem1 13110  bcthlem5 13114  sspval 13319  ajfval 13407  dyadmbl 13700  vitalilem2 13709  vitalilem3 13710  vitali 13713  itg2seq 13842  dvrec 14023  psercn 14264  abelth 14276  logcn 14424  ltbval 14952  opsrle 14954  shex 15296  chex 15311  hmopex 15961  kur14lem7 16707  kur14lem9 16709  dfon2lem7 17078  colinearex 17635  prodex 18304  lteqttos 18677  issubcat 18916  isrocatset 19029  neibastop2lem1 19281  neibastop2lem4 19284  heibor1lem 19595  rngohomval 19659  hsmexlem6 19990  istopon 20088  eldiophb 20193  pellexlem3 20301  pellexlem5 20303  setindtr 20506  aannenlem3 20764  lpival 21059  onfrALTlem3VD 21865  bnj20 22233  bnj53 23012  lcvfbr 23451  cmtfval 23679  cvrfval 23737  lineset 24206  psubspset 24212  psubclset 24404  lautset 24550  pautset 24566  tendoset 25227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3491
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-v 2329  df-in 2644  df-ss 2648
Copyright terms: Public domain