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 1427  cvv 2335   wss 2634
This theorem is referenced by:  zfausab 3476  ord3ex 3511  moabex 3540  opabex 4795  fvclex 4862  abrexexlem1 4864  abrexex 4866  oprabex 4993  oev 5422  sbthlem2 5772  phplem2 5888  phplem4 5890  php 5892  pssnn 5927  ordtypelem1 6029  hartogslem 6037  inf3lem3 6068  hta 6238  aceq3 6323  aceq5lem4 6328  aceq6b 6332  domtriomlem 6440  axdc3lem 6447  axcclem 6454  zorn2lem1 6504  brdom7disj 6524  brdom6disj 6525  unidom 6528  konigthlem 6554  infmap2lem2 6575  gch-kn 6582  niex 6772  enqex 6814  npex 6878  enrex 6961  1arithlem1 9881  1arith 9885  strss 10014  issubgi 10734  symgval 10819  cmpcld 11169  hmph 11238  blfval 11367  qtopbaslem 11449  divcn 11499  evth 11531  phtpyfval 11536  phtpcval 11543  pi1bval 11571  bcthlem1 11647  bcthlem5 11651  sspval 11856  ajfval 11944  vitalilem2 12203  vitalilem3 12204  vitali 12207  itg2seq 12336  shex 13277  chex 13292  hmopex 13942  dfon2lem7 14734  colinearex 15291  prodex 15962  issubcat 16595  isrocatset 16704  2ndcctbss 16941  neibastop2lem1 16982  neibastop2lem4 16985  heibor1lem 17302  heiborlem3 17306  rngohomval 17366  eldiophb 17585  pellexlem4 17702  pellexlem5 17703  pellex 17705  setindtr 17907  onfrALTlem3VD 18552  bnj20 18916  bnj53 19695  cmtfval 20295  cvrfval 20353  lineset 20840  psubspset 20846  psubclset 21039  lautset 21188  pautset 21209  tendoset 21963
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 3454
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 2641  df-ss 2643
Copyright terms: Public domain