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

Theorem ssexi 4308
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 4307 . 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 1721   _Vcvv 2916    C_ wss 3280
This theorem is referenced by:  zfausab  4312  ord3ex  4349  epse  4525  opabex  5923  fvclex  5940  oprabex  6146  tfrlem16  6613  oev  6717  sbthlem2  7177  phplem2  7246  php  7250  pssnn  7286  dffi3  7394  inf3lem3  7541  r0weon  7850  dfac3  7958  dfac5lem4  7963  dfac2  7967  hsmexlem6  8267  domtriomlem  8278  axdc3lem  8286  ac6  8316  brdom7disj  8365  brdom6disj  8366  konigthlem  8399  niex  8714  enqex  8755  npex  8819  enrex  8901  axcnex  8978  reex  9037  nnex  9962  zex  10247  qex  10542  ixxex  10883  ltweuz  11256  1arithlem1  13246  1arith  13250  prdsval  13633  prdsle  13639  sectfval  13932  sscpwex  13970  issubc  13990  isfunc  14016  fullfunc  14058  fthfunc  14059  isfull  14062  isfth  14066  ipoval  14535  letsr  14627  nmznsg  14939  eqgfval  14943  isghm  14961  symgval  15049  ablfac1b  15583  lpival  16271  ltbval  16487  opsrle  16491  xrsle  16676  xrs10  16692  xrge0cmn  16695  znle  16772  cssval  16864  pjfval  16888  istopon  16945  leordtval2  17230  lecldbas  17237  xkoopn  17574  xkouni  17584  xkoccn  17604  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  uzrest  17882  ustfn  18184  ustn0  18203  imasdsf1olem  18356  qtopbaslem  18745  isphtpc  18972  tchex  19129  tchnmfval  19139  bcthlem1  19230  bcthlem5  19234  dyadmbl  19445  itg2seq  19587  lhop1lem  19850  aannenlem3  20200  psercn  20295  abelth  20310  cxpcn2  20583  vmaval  20849  vmaf  20855  sqff1o  20918  musum  20929  vmadivsum  21129  rpvmasumlem  21134  mudivsum  21177  selberglem1  21192  selberglem2  21193  selberg2lem  21197  selberg2  21198  pntrsumo1  21212  selbergr  21215  issubgoi  21851  sspval  22175  ajfval  22263  shex  22667  chex  22682  hmopex  23331  ressplusf  24136  ressmulgnn  24158  inftmrel  24203  isinftm  24204  dmvlsiga  24465  measbase  24504  ismeas  24506  isrnmeas  24507  faeval  24550  ballotlemoex  24696  kur14lem7  24851  kur14lem9  24853  dfon2lem7  25359  colinearex  25898  heibor1lem  26408  rrnval  26426  eldiophb  26705  pellexlem3  26784  pellexlem5  26786  setindtr  26985  cnmsgngrp  27304  onfrALTlem3VD  28708  lsatset  29473  lcvfbr  29503  cmtfvalN  29693  cvrfval  29751  lineset  30220  psubspset  30226  psubclsetN  30418  lautset  30564  pautsetN  30580  tendoset  31241  dicval  31659
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator