HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexi 3719
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 3718 . 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 1522   _Vcvv 2475    C_ wss 2793
This theorem is referenced by:  zfausab  3722  ord3ex  3757  moabex  3787  epse  3927  opabex  5193  fvclex  5273  oprabex  5456  tfrlem16  5864  oev  5968  sbthlem2  6409  phplem2  6525  php  6529  pssnn  6564  dffi3  6666  inf3lem3  6814  r0weon  7122  dfac3  7228  dfac5lem4  7233  dfac2  7237  hsmexlem6  7520  domtriomlem  7531  axdc3lem  7539  ac6  7565  brdom7disj  7632  brdom6disj  7633  konigthlem  7662  niex  7926  enqex  7967  npex  8031  enrex  8113  axcnex  8190  reex  8248  nnex  9130  zex  9402  qex  9697  ixxex  10035  ltweuz  10379  1arithlem1  12075  1arith  12079  prdsval  12441  prdsle  12447  ipoval  12817  letsr  12900  nmznsg  13370  eqgfval  13374  isghm  13392  symgval  13480  ablfac1b  14013  lpival  14702  ltbval  14919  opsrle  14923  xrsle  15101  xrs10  15117  xrge0cmn  15120  znle  15197  cssval  15288  pjfval  15312  istopon  15369  leordtval2  15633  lecldbas  15640  xkoopn  15971  xkouni  15981  xkoccn  16000  xkoco1cn  16038  xkoco2cn  16039  xkococn  16041  xkoinjcn  16068  uzrest  16279  imasdsf1olem  16624  qtopbaslem  16955  isphtpc  17174  tchex  17329  tchnmfval  17339  bcthlem1  17426  bcthlem5  17430  dyadmbl  17635  itg2seq  17777  psercn  18390  abelth  18405  cxpcn2  18676  vmaval  18905  vmaf  18911  sqff1o  18974  musum  18985  vmadivsum  19185  rpvmasumlem  19190  mudivsum  19233  selberglem1  19248  selberglem2  19249  selberg2lem  19253  selberg2  19254  pntrsumo1  19268  selbergr  19271  issubgoi  19510  sspval  19832  ajfval  19920  shex  20324  chex  20339  hmopex  20988  kur14lem7  21617  kur14lem9  21619  dfon2lem7  22015  colinearex  22560  prodex  23121  isrocatset  23780  heibor1lem  24308  rrnval  24326  eldiophb  24613  pellexlem3  24690  pellexlem5  24692  setindtr  24891  aannenlem3  24980  cnmsgngrp  25253  onfrALTlem3VD  25906  bnj20  26280  bnj53  27059  lsatset  27529  lcvfbr  27559  cmtfvalN  27749  cvrfval  27807  lineset  28276  psubspset  28282  psubclsetN  28474  lautset  28620  pautsetN  28636  tendoset  29297  dicval  29715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-sep 3701
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1447  df-sb 1736  df-clab 2052  df-cleq 2057  df-clel 2060  df-v 2477  df-in 2800  df-ss 2804
Copyright terms: Public domain