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

Theorem ssexi 3763
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 3762 . 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 1533   _Vcvv 2512    C_ wss 2830
This theorem is referenced by:  zfausab  3766  ord3ex  3801  moabex  3831  epse  3971  opabex  5237  fvclex  5317  oprabex  5500  tfrlem16  5908  oev  6012  sbthlem2  6453  phplem2  6569  php  6573  pssnn  6608  dffi3  6710  inf3lem3  6858  r0weon  7166  dfac3  7272  dfac5lem4  7277  dfac2  7281  hsmexlem6  7564  domtriomlem  7575  axdc3lem  7583  ac6  7609  brdom7disj  7676  brdom6disj  7677  konigthlem  7706  niex  7970  enqex  8011  npex  8075  enrex  8157  axcnex  8234  reex  8292  nnex  9177  zex  9455  qex  9750  ixxex  10088  ltweuz  10432  1arithlem1  12129  1arith  12133  prdsval  12496  prdsle  12502  ipoval  12872  letsr  12955  nmznsg  13425  eqgfval  13429  isghm  13447  symgval  13535  ablfac1b  14068  lpival  14757  ltbval  14974  opsrle  14978  xrsle  15156  xrs10  15172  xrge0cmn  15175  znle  15252  cssval  15343  pjfval  15367  istopon  15424  leordtval2  15688  lecldbas  15695  xkoopn  16026  xkouni  16036  xkoccn  16055  xkoco1cn  16093  xkoco2cn  16094  xkococn  16096  xkoinjcn  16123  uzrest  16334  imasdsf1olem  16679  qtopbaslem  17010  isphtpc  17229  tchex  17384  tchnmfval  17394  bcthlem1  17481  bcthlem5  17485  dyadmbl  17690  itg2seq  17832  psercn  18445  abelth  18460  cxpcn2  18731  vmaval  18960  vmaf  18966  sqff1o  19029  musum  19040  vmadivsum  19240  rpvmasumlem  19245  mudivsum  19288  selberglem1  19303  selberglem2  19304  selberg2lem  19308  selberg2  19309  pntrsumo1  19323  selbergr  19326  issubgoi  19568  sspval  19890  ajfval  19978  shex  20382  chex  20397  hmopex  21046  kur14lem7  21675  kur14lem9  21677  dfon2lem7  22071  colinearex  22616  prodex  23188  isrocatset  23847  heibor1lem  24427  rrnval  24445  eldiophb  24732  pellexlem3  24809  pellexlem5  24811  setindtr  25010  aannenlem3  25099  cnmsgngrp  25372  onfrALTlem3VD  26063  lsatset  26583  lcvfbr  26613  cmtfvalN  26803  cvrfval  26861  lineset  27330  psubspset  27336  psubclsetN  27528  lautset  27674  pautsetN  27690  tendoset  28351  dicval  28769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1457  df-sb 1748  df-clab 2088  df-cleq 2093  df-clel 2096  df-v 2514  df-in 2837  df-ss 2841
  Copyright terms: Public domain W3C validator