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

Theorem ssexi 4570
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 4569 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 5 1  |-  A  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1870   _Vcvv 3087    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456
This theorem is referenced by:  zfausab  4574  ord3ex  4615  epse  4837  opabex  6149  fvclex  6779  oprabex  6795  tfrlem16  7119  oev  7224  sbthlem2  7689  phplem2  7758  php  7762  pssnn  7796  dffi3  7951  inf3lem3  8135  r0weon  8442  dfac3  8550  dfac5lem4  8555  dfac2  8559  hsmexlem6  8859  domtriomlem  8870  axdc3lem  8878  ac6  8908  brdom7disj  8957  brdom6disj  8958  konigthlem  8991  niex  9305  enqex  9346  npex  9410  enrex  9490  axcnex  9570  reex  9629  nnex  10615  zex  10946  qex  11276  ixxex  11646  ltweuz  12172  prmex  14599  1arithlem1  14830  1arith  14834  prdsval  15312  prdsle  15319  sectfval  15607  sscpwex  15671  issubc  15691  isfunc  15720  fullfunc  15762  fthfunc  15763  isfull  15766  isfth  15770  ipoval  16351  letsr  16424  nmznsg  16812  eqgfval  16816  isghm  16834  symgval  16971  ablfac1b  17638  lpival  18404  ltbval  18630  opsrle  18634  xrsle  18923  xrs10  18942  xrge0cmn  18945  znle  19038  cnmsgngrp  19078  psgninv  19081  cssval  19176  pjfval  19200  istopon  19871  leordtval2  20159  lecldbas  20166  xkoopn  20535  xkouni  20545  xkoccn  20565  xkoco1cn  20603  xkoco2cn  20604  xkococn  20606  xkoinjcn  20633  uzrest  20843  ustfn  21147  ustn0  21166  imasdsf1olem  21319  qtopbaslem  21690  isphtpc  21918  tchex  22084  tchnmfval  22095  bcthlem1  22185  bcthlem5  22189  dyadmbl  22435  itg2seq  22577  lhop1lem  22842  aannenlem3  23151  psercn  23246  abelth  23261  cxpcn2  23551  vmaval  23903  sqff1o  23972  musum  23983  vmadivsum  24183  rpvmasumlem  24188  mudivsum  24231  selberglem1  24246  selberglem2  24247  selberg2lem  24251  selberg2  24252  pntrsumo1  24266  selbergr  24269  iscgrg  24420  isismt  24439  ishlg  24507  ishpg  24657  iscgra  24707  isinag  24732  issubgoi  25883  sspval  26207  ajfval  26295  shex  26700  chex  26714  hmopex  27363  ressplusf  28249  ressmulgnn  28282  inftmrel  28335  isinftm  28336  dmvlsiga  28790  measbase  28858  ismeas  28860  isrnmeas  28861  faeval  28908  eulerpartlemmf  29034  eulerpartlemgvv  29035  signsplypnf  29227  signsply0  29228  afsval  29276  kur14lem7  29723  kur14lem9  29725  mppsval  29998  dfon2lem7  30222  colinearex  30612  poimirlem4  31648  heibor1lem  31845  rrnval  31863  lsatset  32265  lcvfbr  32295  cmtfvalN  32485  cvrfval  32543  lineset  33012  psubspset  33018  psubclsetN  33210  lautset  33356  pautsetN  33372  tendoset  34035  dicval  34453  eldiophb  35308  pellexlem3  35385  pellexlem5  35387  setindtr  35585  onfrALTlem3VD  36924
  Copyright terms: Public domain W3C validator