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

Theorem ssexi 3485
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 3484 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1416  cvv 2324   wss 2634
This theorem is referenced by:  zfausab 3488  ord3ex 3523  moabex 3552  opabex 4848  fvclex 4916  abrexexlem1 4918  abrexex 4920  oprabex 5049  oev 5528  sbthlem2 5893  phplem2 6014  phplem4 6016  php 6018  pssnn 6053  ordtypelem1 6161  hartogslem 6169  inf3lem3 6207  hta 6377  aceq3 6463  aceq5lem4 6468  aceq6b 6472  domtriomlem 6606  axdc3lem 6613  axcclem 6620  zorn2lem1 6669  brdom7disj 6689  brdom6disj 6690  unidom 6693  konigthlem 6719  infmap2lem2 6740  gch-kn 6747  niex 6936  enqex 6978  npex 7042  enrex 7125  1arithlem1 10074  1arith 10078  strss 10221  prdmlelem 10323  eqgfval 10744  isghm 10753  symgval 10808  issubgoi 11452  cmpcld 11881  hmph 11982  blfval 12115  qtopbaslem 12197  divcn 12253  evth 12286  phtpyfval 12296  phtpcval 12303  pi1bval 12335  bcthlem1 12419  bcthlem5 12423  sspval 12628  ajfval 12716  vitalilem2 12975  vitalilem3 12976  vitali 12979  itg2seq 13108  shex 14087  chex 14102  hmopex 14752  kur14lem7 15497  kur14lem9 15499  ltbval 15771  opsrle 15773  dfon2lem7 16003  colinearex 16560  prodex 17234  issubcat 17863  isrocatset 17976  2ndcctbss 18205  neibastop2lem1 18246  neibastop2lem4 18249  heibor1lem 18566  heiborlem3 18570  rngohomval 18630  hsmexlem6 18921  istopon 19012  eldiophb 19078  pellexlem4 19187  pellexlem5 19188  pellex 19190  setindtr 19392  lpival 19886  onfrALTlem3VD 20446  bnj20 20811  bnj53 21590  lcvfbr 22027  cmtfval 22250  cvrfval 22308  lineset 22777  psubspset 22783  psubclset 22975  lautset 23121  pautset 23137  tendoset 23798
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 3466
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 2326  df-in 2641  df-ss 2645
Copyright terms: Public domain