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

Theorem ssexi 3469
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 3468 . 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 1430  _Vcvv 2337   C_ wss 2636
This theorem is referenced by:  zfausab 3472  ord3ex 3507  moabex 3536  opabex 4785  fvclex 4852  abrexexlem1 4854  abrexex 4856  oprabex 4982  oev 5399  sbthlem2 5749  phplem2 5865  phplem4 5867  php 5869  pssnn 5904  ordtypelem1 6006  hartogslem 6014  inf3lem3 6045  hta 6216  aceq3 6301  aceq5lem4 6306  aceq6b 6310  domtriomlem 6418  axdc3lem 6425  axcclem 6432  zorn2lem1 6482  brdom7disj 6502  brdom6disj 6503  unidom 6506  konigthlem 6532  infmap2lem2 6553  gch-kn 6560  niex 6750  enqex 6792  npex 6856  enrex 6939  1arithlem1 9854  1arith 9858  strss 9987  issubgi 10699  symgval 10784  cmpcld 11134  hmph 11203  blfval 11332  qtopbaslem 11414  divcn 11464  evth 11496  phtpyfval 11501  phtpcval 11508  pi1bval 11536  bcthlem1 11612  bcthlem5 11616  sspval 11821  ajfval 11909  vitalilem2 12168  vitalilem3 12169  vitali 12172  itg2seq 12301  shex 13242  chex 13257  hmopex 13907  dfon2lem7 14699  colinearex 15256  prodex 15927  issubcat 16560  isrocatset 16669  2ndcctbss 16906  neibastop2lem1 16947  neibastop2lem4 16950  heibor1lem 17267  heiborlem3 17271  rngohomval 17331  onfrALTlem3VD 17971  bnj20 18335  bnj53 19114  cmtfval 19546  cvrfval 19605  lineset 20127  psubspset 20133  psubclset 20326  lautset 20476  pautset 20497  tendoset 21230
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914  ax-sep 3450
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1350  df-sb 1605  df-clab 1920  df-cleq 1925  df-clel 1928  df-v 2339  df-in 2643  df-ss 2645
Copyright terms: Public domain