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

Theorem ssexi 4053
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 4052 . 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 2725    C_ wss 3075
This theorem is referenced by:  zfausab  4056  ord3ex  4091  epse  4266  opabex  5593  fvclex  5610  oprabex  5810  tfrlem16  6292  oev  6396  sbthlem2  6854  phplem2  6923  php  6927  pssnn  6963  dffi3  7065  inf3lem3  7212  r0weon  7521  dfac3  7629  dfac5lem4  7634  dfac2  7638  hsmexlem6  7938  domtriomlem  7949  axdc3lem  7957  ac6  7988  brdom7disj  8037  brdom6disj  8038  konigthlem  8067  niex  8382  enqex  8423  npex  8487  enrex  8569  axcnex  8646  reex  8705  nnex  9600  zex  9879  qex  10174  ixxex  10512  ltweuz  10867  1arithlem1  12806  1arith  12810  prdsval  13191  prdsle  13197  sectfval  13460  sscpwex  13498  issubc  13518  isfunc  13544  fullfunc  13586  fthfunc  13587  isfull  13590  isfth  13594  ipoval  14063  letsr  14146  nmznsg  14458  eqgfval  14462  isghm  14480  symgval  14568  ablfac1b  15102  lpival  15791  ltbval  16007  opsrle  16011  xrsle  16188  xrs10  16204  xrge0cmn  16207  znle  16284  cssval  16376  pjfval  16400  istopon  16457  leordtval2  16736  lecldbas  16743  xkoopn  17078  xkouni  17088  xkoccn  17107  xkoco1cn  17145  xkoco2cn  17146  xkococn  17148  xkoinjcn  17175  uzrest  17386  imasdsf1olem  17731  qtopbaslem  18061  isphtpc  18286  tchex  18443  tchnmfval  18453  bcthlem1  18540  bcthlem5  18544  dyadmbl  18749  itg2seq  18891  lhop1lem  19154  aannenlem3  19504  psercn  19596  abelth  19611  cxpcn2  19888  vmaval  20117  vmaf  20123  sqff1o  20186  musum  20197  vmadivsum  20397  rpvmasumlem  20402  mudivsum  20445  selberglem1  20460  selberglem2  20461  selberg2lem  20465  selberg2  20466  pntrsumo1  20480  selbergr  20483  issubgoi  20738  sspval  21060  ajfval  21148  shex  21552  chex  21567  hmopex  22216  kur14lem7  22845  kur14lem9  22847  dfon2lem7  23244  colinearex  23788  prodex  24401  isrocatset  25054  heibor1lem  25630  rrnval  25648  eldiophb  25933  pellexlem3  26013  pellexlem5  26015  setindtr  26214  cnmsgngrp  26533  onfrALTlem3VD  27228  lsatset  27744  lcvfbr  27774  cmtfvalN  27964  cvrfval  28022  lineset  28491  psubspset  28497  psubclsetN  28689  lautset  28835  pautsetN  28851  tendoset  29512  dicval  29930
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 1926  ax-ext 2234  ax-sep 4035
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2727  df-in 3082  df-ss 3086
  Copyright terms: Public domain W3C validator