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

Theorem ssexi 4035
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 4034 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 9 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1610   _Vcvv 2712    C_ wss 3058
This theorem is referenced by:  zfausab  4038  ord3ex  4073  epse  4248  opabex  5571  fvclex  5588  oprabex  5787  tfrlem16  6269  oev  6373  sbthlem2  6831  phplem2  6900  php  6904  pssnn  6940  dffi3  7042  inf3lem3  7189  r0weon  7498  dfac3  7606  dfac5lem4  7611  dfac2  7615  hsmexlem6  7915  domtriomlem  7926  axdc3lem  7934  ac6  7965  brdom7disj  8014  brdom6disj  8015  konigthlem  8044  niex  8359  enqex  8400  npex  8464  enrex  8546  axcnex  8623  reex  8682  nnex  9572  zex  9851  qex  10146  ixxex  10484  ltweuz  10839  1arithlem1  12778  1arith  12782  prdsval  13163  prdsle  13169  sectfval  13427  sscpwex  13464  issubc  13484  isfunc  13510  ipoval  13947  letsr  14030  nmznsg  14342  eqgfval  14346  isghm  14364  symgval  14452  ablfac1b  14986  lpival  15675  ltbval  15891  opsrle  15895  xrsle  16072  xrs10  16088  xrge0cmn  16091  znle  16168  cssval  16260  pjfval  16284  istopon  16341  leordtval2  16620  lecldbas  16627  xkoopn  16962  xkouni  16972  xkoccn  16991  xkoco1cn  17029  xkoco2cn  17030  xkococn  17032  xkoinjcn  17059  uzrest  17270  imasdsf1olem  17615  qtopbaslem  17945  isphtpc  18170  tchex  18327  tchnmfval  18337  bcthlem1  18424  bcthlem5  18428  dyadmbl  18633  itg2seq  18775  lhop1lem  19038  aannenlem3  19388  psercn  19480  abelth  19495  cxpcn2  19772  vmaval  20001  vmaf  20007  sqff1o  20070  musum  20081  vmadivsum  20281  rpvmasumlem  20286  mudivsum  20329  selberglem1  20344  selberglem2  20345  selberg2lem  20349  selberg2  20350  pntrsumo1  20364  selbergr  20367  issubgoi  20608  sspval  20930  ajfval  21018  shex  21422  chex  21437  hmopex  22086  kur14lem7  22715  kur14lem9  22717  dfon2lem7  23119  colinearex  23663  prodex  24276  isrocatset  24929  heibor1lem  25505  rrnval  25523  eldiophb  25808  pellexlem3  25888  pellexlem5  25890  setindtr  26089  cnmsgngrp  26408  onfrALTlem3VD  27100  lsatset  27616  lcvfbr  27646  cmtfvalN  27836  cvrfval  27894  lineset  28363  psubspset  28369  psubclsetN  28561  lautset  28707  pautsetN  28723  tendoset  29384  dicval  29802
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-sep 4017
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-v 2714  df-in 3065  df-ss 3069
  Copyright terms: Public domain W3C validator