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

Theorem ssexi 3478
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 3477 . 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 3481  ord3ex 3516  moabex 3545  opabex 4798  fvclex 4865  abrexexlem1 4867  abrexex 4869  oprabex 4995  oev 5423  sbthlem2 5773  phplem2 5889  phplem4 5891  php 5893  pssnn 5928  ordtypelem1 6030  hartogslem 6038  inf3lem3 6069  hta 6239  aceq3 6324  aceq5lem4 6329  aceq6b 6333  domtriomlem 6441  axdc3lem 6448  axcclem 6455  zorn2lem1 6505  brdom7disj 6525  brdom6disj 6526  unidom 6529  konigthlem 6555  infmap2lem2 6576  gch-kn 6583  niex 6773  enqex 6815  npex 6879  enrex 6962  1arithlem1 9879  1arith 9883  strss 10012  issubgi 10732  symgval 10817  cmpcld 11167  hmph 11236  blfval 11365  qtopbaslem 11447  divcn 11497  evth 11529  phtpyfval 11534  phtpcval 11541  pi1bval 11569  bcthlem1 11645  bcthlem5 11649  sspval 11854  ajfval 11942  vitalilem2 12201  vitalilem3 12202  vitali 12205  itg2seq 12334  shex 13275  chex 13290  hmopex 13940  dfon2lem7 14732  colinearex 15289  prodex 15960  issubcat 16593  isrocatset 16702  2ndcctbss 16939  neibastop2lem1 16980  neibastop2lem4 16983  heibor1lem 17300  heiborlem3 17304  rngohomval 17364  onfrALTlem3VD 18004  bnj20 18368  bnj53 19147  cmtfval 19579  cvrfval 19638  lineset 20160  psubspset 20166  psubclset 20359  lautset 20508  pautset 20529  tendoset 21283
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 3459
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