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

Theorem ssexi 4161
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 4160 . 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 1686   _Vcvv 2790    C_ wss 3154
This theorem is referenced by:  zfausab  4165  ord3ex  4202  epse  4378  opabex  5746  fvclex  5763  oprabex  5963  tfrlem16  6411  oev  6515  sbthlem2  6974  phplem2  7043  php  7047  pssnn  7083  dffi3  7186  inf3lem3  7333  r0weon  7642  dfac3  7750  dfac5lem4  7755  dfac2  7759  hsmexlem6  8059  domtriomlem  8070  axdc3lem  8078  ac6  8109  brdom7disj  8158  brdom6disj  8159  konigthlem  8192  niex  8507  enqex  8548  npex  8612  enrex  8694  axcnex  8771  reex  8830  nnex  9754  zex  10035  qex  10330  ixxex  10669  ltweuz  11026  1arithlem1  12972  1arith  12976  prdsval  13357  prdsle  13363  sectfval  13656  sscpwex  13694  issubc  13714  isfunc  13740  fullfunc  13782  fthfunc  13783  isfull  13786  isfth  13790  ipoval  14259  letsr  14351  nmznsg  14663  eqgfval  14667  isghm  14685  symgval  14773  ablfac1b  15307  lpival  15999  ltbval  16215  opsrle  16219  xrsle  16396  xrs10  16412  xrge0cmn  16415  znle  16492  cssval  16584  pjfval  16608  istopon  16665  leordtval2  16944  lecldbas  16951  xkoopn  17286  xkouni  17296  xkoccn  17315  xkoco1cn  17353  xkoco2cn  17354  xkococn  17356  xkoinjcn  17383  uzrest  17594  imasdsf1olem  17939  qtopbaslem  18269  isphtpc  18494  tchex  18651  tchnmfval  18661  bcthlem1  18748  bcthlem5  18752  dyadmbl  18957  itg2seq  19099  lhop1lem  19362  aannenlem3  19712  psercn  19804  abelth  19819  cxpcn2  20088  vmaval  20353  vmaf  20359  sqff1o  20422  musum  20433  vmadivsum  20633  rpvmasumlem  20638  mudivsum  20681  selberglem1  20696  selberglem2  20697  selberg2lem  20701  selberg2  20702  pntrsumo1  20716  selbergr  20719  issubgoi  20979  sspval  21301  ajfval  21389  shex  21793  chex  21808  hmopex  22457  ballotlemoex  23046  ressplusf  23300  ressmulgnn  23310  dmvlsiga  23492  sigagensiga  23504  isrnmeas  23533  coinflippv  23686  kur14lem7  23745  kur14lem9  23747  dfon2lem7  24147  colinearex  24685  prodex  25315  isrocatset  25968  heibor1lem  26544  rrnval  26562  eldiophb  26847  pellexlem3  26927  pellexlem5  26929  setindtr  27128  cnmsgngrp  27447  onfrALTlem3VD  28736  lsatset  29253  lcvfbr  29283  cmtfvalN  29473  cvrfval  29531  lineset  30000  psubspset  30006  psubclsetN  30198  lautset  30344  pautsetN  30360  tendoset  31021  dicval  31439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator