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

Theorem ssexi 4340
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 4339 . 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 1725   _Vcvv 2948    C_ wss 3312
This theorem is referenced by:  zfausab  4344  ord3ex  4381  epse  4557  opabex  5956  fvclex  5973  oprabex  6179  tfrlem16  6646  oev  6750  sbthlem2  7210  phplem2  7279  php  7283  pssnn  7319  dffi3  7428  inf3lem3  7577  r0weon  7886  dfac3  7994  dfac5lem4  7999  dfac2  8003  hsmexlem6  8303  domtriomlem  8314  axdc3lem  8322  ac6  8352  brdom7disj  8401  brdom6disj  8402  konigthlem  8435  niex  8750  enqex  8791  npex  8855  enrex  8937  axcnex  9014  reex  9073  nnex  9998  zex  10283  qex  10578  ixxex  10919  ltweuz  11293  1arithlem1  13283  1arith  13287  prdsval  13670  prdsle  13676  sectfval  13969  sscpwex  14007  issubc  14027  isfunc  14053  fullfunc  14095  fthfunc  14096  isfull  14099  isfth  14103  ipoval  14572  letsr  14664  nmznsg  14976  eqgfval  14980  isghm  14998  symgval  15086  ablfac1b  15620  lpival  16308  ltbval  16524  opsrle  16528  xrsle  16713  xrs10  16729  xrge0cmn  16732  znle  16809  cssval  16901  pjfval  16925  istopon  16982  leordtval2  17268  lecldbas  17275  xkoopn  17613  xkouni  17623  xkoccn  17643  xkoco1cn  17681  xkoco2cn  17682  xkococn  17684  xkoinjcn  17711  uzrest  17921  ustfn  18223  ustn0  18242  imasdsf1olem  18395  qtopbaslem  18784  isphtpc  19011  tchex  19168  tchnmfval  19178  bcthlem1  19269  bcthlem5  19273  dyadmbl  19484  itg2seq  19626  lhop1lem  19889  aannenlem3  20239  psercn  20334  abelth  20349  cxpcn2  20622  vmaval  20888  vmaf  20894  sqff1o  20957  musum  20968  vmadivsum  21168  rpvmasumlem  21173  mudivsum  21216  selberglem1  21231  selberglem2  21232  selberg2lem  21236  selberg2  21237  pntrsumo1  21251  selbergr  21254  issubgoi  21890  sspval  22214  ajfval  22302  shex  22706  chex  22721  hmopex  23370  ressplusf  24175  ressmulgnn  24197  inftmrel  24242  isinftm  24243  dmvlsiga  24504  measbase  24543  ismeas  24545  isrnmeas  24546  faeval  24589  ballotlemoex  24735  kur14lem7  24890  kur14lem9  24892  dfon2lem7  25408  colinearex  25986  heibor1lem  26499  rrnval  26517  eldiophb  26796  pellexlem3  26875  pellexlem5  26877  setindtr  27076  cnmsgngrp  27394  onfrALTlem3VD  28926  lsatset  29715  lcvfbr  29745  cmtfvalN  29935  cvrfval  29993  lineset  30462  psubspset  30468  psubclsetN  30660  lautset  30806  pautsetN  30822  tendoset  31483  dicval  31901
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator