MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexi Unicode version

Theorem ssexi 4289
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
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 4288 . 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 1717   _Vcvv 2899    C_ wss 3263
This theorem is referenced by:  zfausab  4293  ord3ex  4330  epse  4506  opabex  5903  fvclex  5920  oprabex  6126  tfrlem16  6590  oev  6694  sbthlem2  7154  phplem2  7223  php  7227  pssnn  7263  dffi3  7371  inf3lem3  7518  r0weon  7827  dfac3  7935  dfac5lem4  7940  dfac2  7944  hsmexlem6  8244  domtriomlem  8255  axdc3lem  8263  ac6  8293  brdom7disj  8342  brdom6disj  8343  konigthlem  8376  niex  8691  enqex  8732  npex  8796  enrex  8878  axcnex  8955  reex  9014  nnex  9938  zex  10223  qex  10518  ixxex  10859  ltweuz  11228  1arithlem1  13218  1arith  13222  prdsval  13605  prdsle  13611  sectfval  13904  sscpwex  13942  issubc  13962  isfunc  13988  fullfunc  14030  fthfunc  14031  isfull  14034  isfth  14038  ipoval  14507  letsr  14599  nmznsg  14911  eqgfval  14915  isghm  14933  symgval  15021  ablfac1b  15555  lpival  16243  ltbval  16459  opsrle  16463  xrsle  16644  xrs10  16660  xrge0cmn  16663  znle  16740  cssval  16832  pjfval  16856  istopon  16913  leordtval2  17198  lecldbas  17205  xkoopn  17542  xkouni  17552  xkoccn  17572  xkoco1cn  17610  xkoco2cn  17611  xkococn  17613  xkoinjcn  17640  uzrest  17850  ustfn  18152  ustn0  18171  imasdsf1olem  18311  qtopbaslem  18663  isphtpc  18890  tchex  19047  tchnmfval  19057  bcthlem1  19146  bcthlem5  19150  dyadmbl  19359  itg2seq  19501  lhop1lem  19764  aannenlem3  20114  psercn  20209  abelth  20224  cxpcn2  20497  vmaval  20763  vmaf  20769  sqff1o  20832  musum  20843  vmadivsum  21043  rpvmasumlem  21048  mudivsum  21091  selberglem1  21106  selberglem2  21107  selberg2lem  21111  selberg2  21112  pntrsumo1  21126  selbergr  21129  issubgoi  21746  sspval  22070  ajfval  22158  shex  22562  chex  22577  hmopex  23226  ressplusf  24022  ressmulgnn  24034  dmvlsiga  24308  measbase  24347  ismeas  24349  isrnmeas  24350  faeval  24391  ballotlemoex  24522  kur14lem7  24677  kur14lem9  24679  dfon2lem7  25169  colinearex  25708  heibor1lem  26209  rrnval  26227  eldiophb  26506  pellexlem3  26585  pellexlem5  26587  setindtr  26786  cnmsgngrp  27105  onfrALTlem3VD  28340  lsatset  29105  lcvfbr  29135  cmtfvalN  29325  cvrfval  29383  lineset  29852  psubspset  29858  psubclsetN  30050  lautset  30196  pautsetN  30212  tendoset  30873  dicval  31291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator