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

Theorem ssexi 3473
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 3472 . 2
41, 3ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wcel 1415  cvv 2322   wss 2632
This theorem is referenced by:  zfausab 3476  ord3ex 3511  moabex 3540  opabex 4814  fvclex 4881  abrexexlem1 4883  abrexex 4885  oprabex 5013  oev 5483  sbthlem2 5843  phplem2 5959  phplem4 5961  php 5963  pssnn 5998  ordtypelem1 6105  hartogslem 6113  inf3lem3 6144  hta 6314  aceq3 6400  aceq5lem4 6405  aceq6b 6409  domtriomlem 6543  axdc3lem 6550  axcclem 6557  zorn2lem1 6606  brdom7disj 6626  brdom6disj 6627  unidom 6630  konigthlem 6656  infmap2lem2 6677  gch-kn 6684  niex 6873  enqex 6915  npex 6979  enrex 7062  1arithlem1 10007  1arith 10011  strss 10154  prdmlelem 10256  eqgfval 10655  isghm 10664  symgval 10716  issubgoi 11352  cmpcld 11777  hmph 11846  blfval 11974  qtopbaslem 12056  divcn 12106  evth 12138  phtpyfval 12143  phtpcval 12150  pi1bval 12178  bcthlem1 12254  bcthlem5 12258  sspval 12463  ajfval 12551  vitalilem2 12810  vitalilem3 12811  vitali 12814  itg2seq 12943  shex 13887  chex 13902  hmopex 14552  dfon2lem7 15652  colinearex 16209  prodex 16893  issubcat 17525  isrocatset 17638  2ndcctbss 17875  neibastop2lem1 17916  neibastop2lem4 17919  heibor1lem 18236  heiborlem3 18240  rngohomval 18300  eldiophb 18518  pellexlem4 18630  pellexlem5 18631  pellex 18633  setindtr 18835  lpival 19267  onfrALTlem3VD 19830  bnj20 20195  bnj53 20974  lcvfbr 21406  cmtfval 21617  cvrfval 21675  lineset 22144  psubspset 22150  psubclset 22342  lautset 22488  pautset 22504  tendoset 23165
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-sep 3454
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-v 2324  df-in 2639  df-ss 2641
Copyright terms: Public domain