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

Theorem ssexi 4056
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 4055 . 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 2727    C_ wss 3078
This theorem is referenced by:  zfausab  4059  ord3ex  4094  epse  4269  opabex  5596  fvclex  5613  oprabex  5813  tfrlem16  6295  oev  6399  sbthlem2  6857  phplem2  6926  php  6930  pssnn  6966  dffi3  7068  inf3lem3  7215  r0weon  7524  dfac3  7632  dfac5lem4  7637  dfac2  7641  hsmexlem6  7941  domtriomlem  7952  axdc3lem  7960  ac6  7991  brdom7disj  8040  brdom6disj  8041  konigthlem  8070  niex  8385  enqex  8426  npex  8490  enrex  8572  axcnex  8649  reex  8708  nnex  9632  zex  9912  qex  10207  ixxex  10545  ltweuz  10902  1arithlem1  12844  1arith  12848  prdsval  13229  prdsle  13235  sectfval  13498  sscpwex  13536  issubc  13556  isfunc  13582  fullfunc  13624  fthfunc  13625  isfull  13628  isfth  13632  ipoval  14101  letsr  14184  nmznsg  14496  eqgfval  14500  isghm  14518  symgval  14606  ablfac1b  15140  lpival  15829  ltbval  16045  opsrle  16049  xrsle  16226  xrs10  16242  xrge0cmn  16245  znle  16322  cssval  16414  pjfval  16438  istopon  16495  leordtval2  16774  lecldbas  16781  xkoopn  17116  xkouni  17126  xkoccn  17145  xkoco1cn  17183  xkoco2cn  17184  xkococn  17186  xkoinjcn  17213  uzrest  17424  imasdsf1olem  17769  qtopbaslem  18099  isphtpc  18324  tchex  18481  tchnmfval  18491  bcthlem1  18578  bcthlem5  18582  dyadmbl  18787  itg2seq  18929  lhop1lem  19192  aannenlem3  19542  psercn  19634  abelth  19649  cxpcn2  19954  vmaval  20183  vmaf  20189  sqff1o  20252  musum  20263  vmadivsum  20463  rpvmasumlem  20468  mudivsum  20511  selberglem1  20526  selberglem2  20527  selberg2lem  20531  selberg2  20532  pntrsumo1  20546  selbergr  20549  issubgoi  20807  sspval  21129  ajfval  21217  shex  21621  chex  21636  hmopex  22285  kur14lem7  22914  kur14lem9  22916  dfon2lem7  23313  colinearex  23857  prodex  24470  isrocatset  25123  heibor1lem  25699  rrnval  25717  eldiophb  26002  pellexlem3  26082  pellexlem5  26084  setindtr  26283  cnmsgngrp  26602  onfrALTlem3VD  27353  lsatset  27869  lcvfbr  27899  cmtfvalN  28089  cvrfval  28147  lineset  28616  psubspset  28622  psubclsetN  28814  lautset  28960  pautsetN  28976  tendoset  29637  dicval  30055
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 4038
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 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator