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

Theorem ssexi 3716
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 3715 . 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 1519   _Vcvv 2472    C_ wss 2790
This theorem is referenced by:  zfausab  3719  ord3ex  3754  moabex  3784  epse  3924  opabex  5188  fvclex  5268  oprabex  5451  tfrlem16  5858  oev  5962  sbthlem2  6403  phplem2  6519  php  6523  pssnn  6558  dffi3  6660  inf3lem3  6808  r0weon  7116  dfac3  7222  dfac5lem4  7227  dfac2  7231  hsmexlem6  7514  domtriomlem  7525  axdc3lem  7533  ac6  7559  brdom7disj  7626  brdom6disj  7627  konigthlem  7656  niex  7919  enqex  7960  npex  8024  enrex  8106  axcnex  8183  reex  8241  nnex  8884  zex  9132  qex  9417  ixxex  9688  ltweuz  10019  1arithlem1  11474  1arith  11478  prdsval  11840  prdsle  11846  ipoval  12216  letsr  12299  nmznsg  12769  eqgfval  12773  isghm  12791  symgval  12879  ablfac1b  13410  lpival  14096  ltbval  14313  opsrle  14317  xrsle  14495  xrs10  14511  xrge0cmn  14514  znle  14591  cssval  14681  pjfval  14705  istopon  14762  leordtval2  15026  lecldbas  15033  xkoopn  15364  xkouni  15374  xkoccn  15393  xkoco1cn  15431  xkoco2cn  15432  xkococn  15434  xkoinjcn  15461  uzrest  15672  imasdsf1olem  16017  qtopbaslem  16348  isphtpc  16566  tchex  16721  tchnmfval  16731  bcthlem1  16818  bcthlem5  16822  dyadmbl  17027  itg2seq  17169  psercn  17761  abelth  17776  sqff1o  18247  musum  18251  issubgoi  18560  sspval  18882  ajfval  18970  shex  19374  chex  19389  hmopex  20038  kur14lem7  20667  kur14lem9  20669  dfon2lem7  21086  colinearex  21631  prodex  22191  isrocatset  22850  heibor1lem  23345  rrnval  23363  eldiophb  23651  pellexlem3  23758  pellexlem5  23760  setindtr  23959  aannenlem3  24048  cnmsgngrp  24321  onfrALTlem3VD  24975  bnj20  25349  bnj53  26128  lsatset  26598  lcvfbr  26628  cmtfvalN  26818  cvrfval  26876  lineset  27345  psubspset  27351  psubclsetN  27543  lautset  27689  pautsetN  27705  tendoset  28366  dicval  28784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-sep 3698
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1444  df-sb 1733  df-clab 2049  df-cleq 2054  df-clel 2057  df-v 2474  df-in 2797  df-ss 2801
Copyright terms: Public domain