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

Theorem ssexi 3733
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 3732 . 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 1538   _Vcvv 2492    C_ wss 2810
This theorem is referenced by:  zfausab  3736  ord3ex  3771  moabex  3801  epse  3941  opabex  5188  fvclex  5267  oprabex  5449  tfrlem16  5856  oev  5957  sbthlem2  6396  phplem2  6512  php  6516  pssnn  6549  dffi3  6646  inf3lem3  6794  r0weon  7102  dfac3  7208  dfac5lem4  7213  dfac2  7217  hsmexlem6  7500  domtriomlem  7511  axdc3lem  7519  ac6  7545  brdom7disj  7612  brdom6disj  7613  konigthlem  7642  niex  7905  enqex  7946  npex  8010  enrex  8092  axcnex  8169  reex  8227  nnex  8868  zex  9116  qex  9401  ixxex  9669  ltweuz  9998  1arithlem1  11425  1arith  11429  prdsval  11785  prdsle  11791  ipoval  12110  letsr  12183  nmznsg  12570  eqgfval  12574  isghm  12592  symgval  12675  lpival  13671  ltbval  13887  opsrle  13891  xrsle  14069  xrs10  14085  xrge0cmn  14088  znle  14164  cssval  14242  pjfval  14264  istopon  14406  leordtval2  14670  lecldbas  14677  cmpcld  14854  xkoopn  15008  xkouni  15018  xkoccn  15037  xkoco1cn  15075  xkoco2cn  15076  xkococn  15078  xkoinjcn  15105  uzrest  15316  imasdsf1olem  15661  qtopbaslem  15992  isphtpc  16210  tchex  16365  tchnmfval  16375  bcthlem1  16462  bcthlem5  16466  dyadmbl  16671  itg2seq  16813  psercn  17405  abelth  17420  sqff1o  17889  musum  17893  issubgoi  18198  sspval  18520  ajfval  18608  shex  19012  chex  19027  hmopex  19676  kur14lem7  20310  kur14lem9  20312  dfon2lem7  20735  colinearex  21282  prodex  21849  isrocatset  22511  heibor1lem  22981  rrnval  22999  eldiophb  23288  pellexlem3  23395  pellexlem5  23397  setindtr  23600  aannenlem3  23691  cnmsgngrp  23964  onfrALTlem3VD  24649  bnj20  25023  bnj53  25802  lsatset  26272  lcvfbr  26303  cmtfvalN  26493  cvrfval  26551  lineset  27020  psubspset  27026  psubclsetN  27218  lautset  27364  pautsetN  27380  tendoset  28041  dicval  28459
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-v 2494  df-in 2817  df-ss 2821
Copyright terms: Public domain