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

Theorem ssexi 3491
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 3490 . 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 3494  ord3ex 3529  moabex 3558  opabex 4795  fvclex 4862  abrexexlem1 4864  abrexex 4866  oprabex 4992  oev 5379  sbthlem2 5729  phplem2 5845  phplem4 5847  php 5849  pssnn 5884  ordtypelem1 5984  ordtypelem7 5990  hartogslem 5992  inf3lem3 6023  hta 6194  aceq3 6290  aceq5lem4 6295  aceq6b 6299  domtriomlem 6405  axdc3lem 6412  axcclem 6419  numthlem 6464  zorn2lem1 6469  brdom7disj 6489  brdom6disj 6490  unidom 6493  konigthlem 6519  infmap2lem2 6540  gch-kn 6547  niex 6726  enqex 6768  npex 6832  enrex 6915  isprm2lem 9627  1arithlem1 9757  1arith 9761  strss 9855  issubgi 10523  symgval 10608  cmpcld 10950  hmph 11011  blfval 11140  qtopbaslem 11221  phtpyfval 11302  phtpcval 11309  pi1bval 11337  bcthlem1 11413  bcthlem5 11417  sspval 11623  ajfval 11711  shex 12253  chex 12268  hmopex 12918  vitalilem2 13692  vitali 13693  dfon2lem7 13998  colinearex 14555  prodex 15232  issubcat 15871  isrocatset 16008  2ndcctbss 16252  neibastop2lem1 16293  neibastop2lem4 16296  heibor1lem 16617  heiborlem3 16621  rngohomval 16681  onfrALTlem3VD 17323  bnj20 17687  bnj53 18466  cmtfval 18898  cvrfval 18957  lineset 19480  psubspset 19486  psubclset 19679  lautset 19829  pautset 19850  tendoset 20580
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 3472
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