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

Theorem ssexi 3729
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 3728 . 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 1526   _Vcvv 2480    C_ wss 2798
This theorem is referenced by:  zfausab  3732  ord3ex  3767  moabex  3797  epse  3937  opabex  5203  fvclex  5283  oprabex  5466  tfrlem16  5874  oev  5978  sbthlem2  6419  phplem2  6535  php  6539  pssnn  6574  dffi3  6676  inf3lem3  6824  r0weon  7132  dfac3  7238  dfac5lem4  7243  dfac2  7247  hsmexlem6  7530  domtriomlem  7541  axdc3lem  7549  ac6  7575  brdom7disj  7642  brdom6disj  7643  konigthlem  7672  niex  7936  enqex  7977  npex  8041  enrex  8123  axcnex  8200  reex  8258  nnex  9143  zex  9421  qex  9716  ixxex  10054  ltweuz  10398  1arithlem1  12095  1arith  12099  prdsval  12462  prdsle  12468  ipoval  12838  letsr  12921  nmznsg  13391  eqgfval  13395  isghm  13413  symgval  13501  ablfac1b  14034  lpival  14723  ltbval  14940  opsrle  14944  xrsle  15122  xrs10  15138  xrge0cmn  15141  znle  15218  cssval  15309  pjfval  15333  istopon  15390  leordtval2  15654  lecldbas  15661  xkoopn  15992  xkouni  16002  xkoccn  16021  xkoco1cn  16059  xkoco2cn  16060  xkococn  16062  xkoinjcn  16089  uzrest  16300  imasdsf1olem  16645  qtopbaslem  16976  isphtpc  17195  tchex  17350  tchnmfval  17360  bcthlem1  17447  bcthlem5  17451  dyadmbl  17656  itg2seq  17798  psercn  18411  abelth  18426  cxpcn2  18697  vmaval  18926  vmaf  18932  sqff1o  18995  musum  19006  vmadivsum  19206  rpvmasumlem  19211  mudivsum  19254  selberglem1  19269  selberglem2  19270  selberg2lem  19274  selberg2  19275  pntrsumo1  19289  selbergr  19292  issubgoi  19533  sspval  19855  ajfval  19943  shex  20347  chex  20362  hmopex  21011  kur14lem7  21640  kur14lem9  21642  dfon2lem7  22036  colinearex  22581  prodex  23143  isrocatset  23802  heibor1lem  24363  rrnval  24381  eldiophb  24668  pellexlem3  24745  pellexlem5  24747  setindtr  24946  aannenlem3  25035  cnmsgngrp  25308  onfrALTlem3VD  25965  bnj20  26340  bnj53  27119  lsatset  27585  lcvfbr  27615  cmtfvalN  27805  cvrfval  27863  lineset  28332  psubspset  28338  psubclsetN  28530  lautset  28676  pautsetN  28692  tendoset  29353  dicval  29771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594  ax-16 1780  ax-ext 2051  ax-sep 3711
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1451  df-sb 1741  df-clab 2057  df-cleq 2062  df-clel 2065  df-v 2482  df-in 2805  df-ss 2809
  Copyright terms: Public domain W3C validator