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

Theorem ssexi 3477
Description: The subset of a set is also a set.
Hypotheses
Ref Expression
ssexi.1 |- B e. _V
ssexi.2 |- A C_ B
Assertion
Ref Expression
ssexi |- A e. _V

Proof of Theorem ssexi
StepHypRef Expression
1 ssexi.2 . 2 |- A C_ B
2 ssexi.1 . . 3 |- B e. _V
32ssex 3476 . 2 |- (A C_ B -> A e. _V)
41, 3ax-mp 8 1 |- A e. _V
Colors of variables: wff set class
Syntax hints:   e. wcel 1436  _Vcvv 2343   C_ wss 2642
This theorem is referenced by:  zfausab 3480  ord3ex 3515  moabex 3544  opabex 4793  fvclex 4860  abrexexlem1 4862  abrexex 4864  oprabex 4990  oev 5408  sbthlem2 5758  phplem2 5874  phplem4 5876  php 5878  pssnn 5913  ordtypelem1 6015  hartogslem 6023  inf3lem3 6054  hta 6224  aceq3 6309  aceq5lem4 6314  aceq6b 6318  domtriomlem 6426  axdc3lem 6433  axcclem 6440  zorn2lem1 6490  brdom7disj 6510  brdom6disj 6511  unidom 6514  konigthlem 6540  infmap2lem2 6561  gch-kn 6568  niex 6758  enqex 6800  npex 6864  enrex 6947  1arithlem1 9862  1arith 9866  strss 9995  issubgi 10710  symgval 10795  cmpcld 11145  hmph 11214  blfval 11343  qtopbaslem 11425  divcn 11475  evth 11507  phtpyfval 11512  phtpcval 11519  pi1bval 11547  bcthlem1 11623  bcthlem5 11627  sspval 11832  ajfval 11920  vitalilem2 12179  vitalilem3 12180  vitali 12183  itg2seq 12312  shex 13253  chex 13268  hmopex 13918  dfon2lem7 14710  colinearex 15267  prodex 15938  issubcat 16571  isrocatset 16680  2ndcctbss 16917  neibastop2lem1 16958  neibastop2lem4 16961  heibor1lem 17278  heiborlem3 17282  rngohomval 17342  onfrALTlem3VD 17982  bnj20 18346  bnj53 19125  cmtfval 19557  cvrfval 19616  lineset 20138  psubspset 20144  psubclset 20337  lautset 20486  pautset 20507  tendoset 21251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-sep 3458
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-v 2345  df-in 2649  df-ss 2651
Copyright terms: Public domain