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

Theorem ssexi 3493
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 3492 . 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 1459  _Vcvv 2365   C_ wss 2662
This theorem is referenced by:  zfausab 3496  ord3ex 3531  moabex 3560  opabex 4800  fvclex 4867  abrexexlem1 4869  abrexex 4871  oprabex 4997  oev 5385  sbthlem2 5735  phplem2 5851  phplem4 5853  php 5855  pssnn 5890  ordtypelem1 5990  ordtypelem7 5996  hartogslem 5998  inf3lem3 6029  hta 6200  aceq3 6296  aceq5lem4 6301  aceq6b 6305  domtriomlem 6411  axdc3lem 6418  axcclem 6425  numthlem 6470  zorn2lem1 6475  brdom7disj 6495  brdom6disj 6496  unidom 6499  konigthlem 6525  infmap2lem2 6546  gch-kn 6553  niex 6732  enqex 6774  npex 6838  enrex 6921  isprm2lem 9643  1arithlem1 9773  1arith 9777  strss 9871  issubgi 10543  symgval 10628  cmpcld 10976  hmph 11038  blfval 11167  qtopbaslem 11248  phtpyfval 11331  phtpcval 11338  pi1bval 11366  bcthlem1 11442  bcthlem5 11446  sspval 11652  ajfval 11740  shex 12314  chex 12329  hmopex 12979  vitalilem2 13860  vitali 13861  dfon2lem7 14219  colinearex 14776  prodex 15452  issubcat 16088  isrocatset 16225  2ndcctbss 16463  neibastop2lem1 16504  neibastop2lem4 16507  heibor1lem 16828  heiborlem3 16832  rngohomval 16892  onfrALTlem3VD 17534  bnj20 17898  bnj53 18677  cmtfval 19109  cvrfval 19168  lineset 19691  psubspset 19697  psubclset 19890  lautset 20040  pautset 20061  tendoset 20791
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-sep 3474
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-v 2367  df-in 2669  df-ss 2671
Copyright terms: Public domain