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

Theorem ssexi 4569
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 4568 . 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 1872   _Vcvv 3080    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450
This theorem is referenced by:  zfausab  4573  ord3ex  4614  epse  4836  opabex  6150  fvclex  6780  oprabex  6796  tfrlem16  7123  oev  7228  sbthlem2  7693  phplem2  7762  php  7766  pssnn  7800  dffi3  7955  inf3lem3  8145  r0weon  8452  dfac3  8560  dfac5lem4  8565  dfac2  8569  hsmexlem6  8869  domtriomlem  8880  axdc3lem  8888  ac6  8918  brdom7disj  8967  brdom6disj  8968  konigthlem  9001  niex  9314  enqex  9355  npex  9419  enrex  9499  axcnex  9579  reex  9638  nnex  10623  zex  10954  qex  11284  ixxex  11654  ltweuz  12182  prmex  14628  1arithlem1  14867  1arith  14871  prdsval  15353  prdsle  15360  sectfval  15656  sscpwex  15720  issubc  15740  isfunc  15769  fullfunc  15811  fthfunc  15812  isfull  15815  isfth  15819  ipoval  16400  letsr  16473  nmznsg  16861  eqgfval  16865  isghm  16883  symgval  17020  ablfac1b  17703  lpival  18469  ltbval  18695  opsrle  18699  xrsle  18988  xrs10  19007  xrge0cmn  19010  znle  19106  cnmsgngrp  19146  psgninv  19149  cssval  19244  pjfval  19268  istopon  19939  leordtval2  20227  lecldbas  20234  xkoopn  20603  xkouni  20613  xkoccn  20633  xkoco1cn  20671  xkoco2cn  20672  xkococn  20674  xkoinjcn  20701  uzrest  20911  ustfn  21215  ustn0  21234  imasdsf1olem  21387  qtopbaslem  21778  isphtpc  22024  tchex  22190  tchnmfval  22201  bcthlem1  22291  bcthlem5  22295  dyadmbl  22557  itg2seq  22699  lhop1lem  22964  aannenlem3  23285  psercn  23380  abelth  23395  cxpcn2  23685  vmaval  24039  sqff1o  24108  musum  24119  vmadivsum  24319  rpvmasumlem  24324  mudivsum  24367  selberglem1  24382  selberglem2  24383  selberg2lem  24387  selberg2  24388  pntrsumo1  24402  selbergr  24405  iscgrg  24556  isismt  24578  ishlg  24646  ishpg  24800  iscgra  24850  isinag  24878  isleag  24882  issubgoi  26037  sspval  26361  ajfval  26449  shex  26864  chex  26878  hmopex  27527  ressplusf  28419  ressmulgnn  28453  inftmrel  28505  isinftm  28506  dmvlsiga  28960  measbase  29028  ismeas  29030  isrnmeas  29031  faeval  29078  eulerpartlemmf  29217  eulerpartlemgvv  29218  signsplypnf  29448  signsply0  29449  afsval  29497  kur14lem7  29944  kur14lem9  29946  mppsval  30219  dfon2lem7  30443  colinearex  30833  poimirlem4  31909  heibor1lem  32106  rrnval  32124  lsatset  32526  lcvfbr  32556  cmtfvalN  32746  cvrfval  32804  lineset  33273  psubspset  33279  psubclsetN  33471  lautset  33617  pautsetN  33633  tendoset  34296  dicval  34714  eldiophb  35569  pellexlem3  35646  pellexlem5  35648  setindtr  35850  onfrALTlem3VD  37258
  Copyright terms: Public domain W3C validator