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

Theorem ssexi 4133
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 4132 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 10 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2763    C_ wss 3127
This theorem is referenced by:  zfausab  4137  ord3ex  4172  epse  4348  opabex  5678  fvclex  5695  oprabex  5895  tfrlem16  6377  oev  6481  sbthlem2  6940  phplem2  7009  php  7013  pssnn  7049  dffi3  7152  inf3lem3  7299  r0weon  7608  dfac3  7716  dfac5lem4  7721  dfac2  7725  hsmexlem6  8025  domtriomlem  8036  axdc3lem  8044  ac6  8075  brdom7disj  8124  brdom6disj  8125  konigthlem  8158  niex  8473  enqex  8514  npex  8578  enrex  8660  axcnex  8737  reex  8796  nnex  9720  zex  10001  qex  10296  ixxex  10634  ltweuz  10991  1arithlem1  12933  1arith  12937  prdsval  13318  prdsle  13324  sectfval  13617  sscpwex  13655  issubc  13675  isfunc  13701  fullfunc  13743  fthfunc  13744  isfull  13747  isfth  13751  ipoval  14220  letsr  14312  nmznsg  14624  eqgfval  14628  isghm  14646  symgval  14734  ablfac1b  15268  lpival  15960  ltbval  16176  opsrle  16180  xrsle  16357  xrs10  16373  xrge0cmn  16376  znle  16453  cssval  16545  pjfval  16569  istopon  16626  leordtval2  16905  lecldbas  16912  xkoopn  17247  xkouni  17257  xkoccn  17276  xkoco1cn  17314  xkoco2cn  17315  xkococn  17317  xkoinjcn  17344  uzrest  17555  imasdsf1olem  17900  qtopbaslem  18230  isphtpc  18455  tchex  18612  tchnmfval  18622  bcthlem1  18709  bcthlem5  18713  dyadmbl  18918  itg2seq  19060  lhop1lem  19323  aannenlem3  19673  psercn  19765  abelth  19780  cxpcn2  20049  vmaval  20314  vmaf  20320  sqff1o  20383  musum  20394  vmadivsum  20594  rpvmasumlem  20599  mudivsum  20642  selberglem1  20657  selberglem2  20658  selberg2lem  20662  selberg2  20663  pntrsumo1  20677  selbergr  20680  issubgoi  20938  sspval  21260  ajfval  21348  shex  21752  chex  21767  hmopex  22416  ballotlemoex  23006  kur14lem7  23116  kur14lem9  23118  dfon2lem7  23515  colinearex  24059  prodex  24672  isrocatset  25325  heibor1lem  25901  rrnval  25919  eldiophb  26204  pellexlem3  26284  pellexlem5  26286  setindtr  26485  cnmsgngrp  26804  onfrALTlem3VD  27796  lsatset  28430  lcvfbr  28460  cmtfvalN  28650  cvrfval  28708  lineset  29177  psubspset  29183  psubclsetN  29375  lautset  29521  pautsetN  29537  tendoset  30198  dicval  30616
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator