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

Theorem ssexi 3500
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 3499 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1416  cvv 2326   wss 2636
This theorem is referenced by:  zfausab 3503  ord3ex 3538  moabex 3567  opabex 4868  fvclex 4936  abrexexlem1 4938  abrexex 4940  oprabex 5074  oev 5560  sbthlem2 5930  phplem2 6052  phplem4 6054  php 6056  pssnn 6092  ordtypelem1 6202  hartogslem 6210  inf3lem3 6248  hta 6418  aceq3 6506  aceq5lem4 6511  aceq6b 6515  domtriomlem 6650  axdc3lem 6657  axcclem 6664  zorn2lem1 6713  brdom7disj 6733  brdom6disj 6734  unidom 6737  konigthlem 6763  infmap2lem2 6784  gch-kn 6791  niex 6980  enqex 7022  npex 7086  enrex 7169  1arithlem1 10175  1arith 10179  strss 10322  prdmlelem 10424  eqgfval 10896  isghm 10905  symgval 10960  issubgoi 11644  cmpcld 12126  2ndcctbss 12181  xkoopn 12279  xkouni 12285  xkoccn 12293  xkoco1cn 12323  xkoco2cn 12324  xkococn 12326  xkoinjcn 12353  hmph 12388  blfval 12551  qtopbaslem 12636  divcn 12699  evth 12732  isphtpc 12766  pi1bval 12803  bcthlem1 12864  bcthlem5 12868  sspval 13073  ajfval 13161  dyadmbl 13459  vitalilem2 13468  vitalilem3 13469  vitali 13472  itg2seq 13601  dvrec 13781  psercn 14022  abelth 14034  logcn 14178  shex 14788  chex 14803  hmopex 15453  kur14lem7 16198  kur14lem9 16200  ltbval 16541  opsrle 16543  dfon2lem7 16773  colinearex 17330  prodex 17999  issubcat 18613  isrocatset 18726  neibastop2lem1 18978  neibastop2lem4 18981  heibor1lem 19294  heiborlem3 19298  rngohomval 19358  hsmexlem6 19644  istopon 19735  eldiophb 19801  pellexlem4 19910  pellexlem5 19911  pellex 19913  setindtr 20114  lpival 20601  onfrALTlem3VD 21176  bnj20 21544  bnj53 22323  lcvfbr 22762  cmtfval 22990  cvrfval 23048  lineset 23517  psubspset 23523  psubclset 23715  lautset 23861  pautset 23877  tendoset 24538
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 3481
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 2328  df-in 2643  df-ss 2647
Copyright terms: Public domain