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

Theorem ssexi 3725
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 3724 . 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 2476    C_ wss 2794
This theorem is referenced by:  zfausab  3728  ord3ex  3763  moabex  3793  epse  3933  opabex  5199  fvclex  5279  oprabex  5462  tfrlem16  5870  oev  5974  sbthlem2  6415  phplem2  6531  php  6535  pssnn  6570  dffi3  6672  inf3lem3  6820  r0weon  7128  dfac3  7234  dfac5lem4  7239  dfac2  7243  hsmexlem6  7526  domtriomlem  7537  axdc3lem  7545  ac6  7571  brdom7disj  7638  brdom6disj  7639  konigthlem  7668  niex  7932  enqex  7973  npex  8037  enrex  8119  axcnex  8196  reex  8254  nnex  9139  zex  9417  qex  9712  ixxex  10050  ltweuz  10394  1arithlem1  12091  1arith  12095  prdsval  12458  prdsle  12464  ipoval  12834  letsr  12917  nmznsg  13387  eqgfval  13391  isghm  13409  symgval  13497  ablfac1b  14030  lpival  14719  ltbval  14936  opsrle  14940  xrsle  15118  xrs10  15134  xrge0cmn  15137  znle  15214  cssval  15305  pjfval  15329  istopon  15386  leordtval2  15650  lecldbas  15657  xkoopn  15988  xkouni  15998  xkoccn  16017  xkoco1cn  16055  xkoco2cn  16056  xkococn  16058  xkoinjcn  16085  uzrest  16296  imasdsf1olem  16641  qtopbaslem  16972  isphtpc  17191  tchex  17346  tchnmfval  17356  bcthlem1  17443  bcthlem5  17447  dyadmbl  17652  itg2seq  17794  psercn  18407  abelth  18422  cxpcn2  18693  vmaval  18922  vmaf  18928  sqff1o  18991  musum  19002  vmadivsum  19202  rpvmasumlem  19207  mudivsum  19250  selberglem1  19265  selberglem2  19266  selberg2lem  19270  selberg2  19271  pntrsumo1  19285  selbergr  19288  issubgoi  19529  sspval  19851  ajfval  19939  shex  20343  chex  20358  hmopex  21007  kur14lem7  21636  kur14lem9  21638  dfon2lem7  22032  colinearex  22577  prodex  23138  isrocatset  23797  heibor1lem  24325  rrnval  24343  eldiophb  24630  pellexlem3  24707  pellexlem5  24709  setindtr  24908  aannenlem3  24997  cnmsgngrp  25270  onfrALTlem3VD  25931  bnj20  26305  bnj53  27084  lsatset  27550  lcvfbr  27580  cmtfvalN  27770  cvrfval  27828  lineset  28297  psubspset  28303  psubclsetN  28495  lautset  28641  pautsetN  28657  tendoset  29318  dicval  29736
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 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-sep 3707
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1447  df-sb 1737  df-clab 2053  df-cleq 2058  df-clel 2061  df-v 2478  df-in 2801  df-ss 2805
Copyright terms: Public domain