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

Theorem ssexi 3717
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 3716 . 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 1520   _Vcvv 2473    C_ wss 2791
This theorem is referenced by:  zfausab  3720  ord3ex  3755  moabex  3785  epse  3925  opabex  5189  fvclex  5269  oprabex  5452  tfrlem16  5860  oev  5964  sbthlem2  6405  phplem2  6521  php  6525  pssnn  6560  dffi3  6662  inf3lem3  6810  r0weon  7118  dfac3  7224  dfac5lem4  7229  dfac2  7233  hsmexlem6  7516  domtriomlem  7527  axdc3lem  7535  ac6  7561  brdom7disj  7628  brdom6disj  7629  konigthlem  7658  niex  7921  enqex  7962  npex  8026  enrex  8108  axcnex  8185  reex  8243  nnex  8888  zex  9136  qex  9422  ixxex  9693  ltweuz  10031  1arithlem1  11541  1arith  11545  prdsval  11907  prdsle  11913  ipoval  12283  letsr  12366  nmznsg  12836  eqgfval  12840  isghm  12858  symgval  12946  ablfac1b  13477  lpival  14165  ltbval  14382  opsrle  14386  xrsle  14564  xrs10  14580  xrge0cmn  14583  znle  14660  cssval  14751  pjfval  14775  istopon  14832  leordtval2  15096  lecldbas  15103  xkoopn  15434  xkouni  15444  xkoccn  15463  xkoco1cn  15501  xkoco2cn  15502  xkococn  15504  xkoinjcn  15531  uzrest  15742  imasdsf1olem  16087  qtopbaslem  16418  isphtpc  16636  tchex  16791  tchnmfval  16801  bcthlem1  16888  bcthlem5  16892  dyadmbl  17097  itg2seq  17239  psercn  17832  abelth  17847  cxpcn2  18074  vmaval  18299  vmaf  18305  sqff1o  18368  musum  18377  vmadivsum  18563  rpvmasumlem  18566  dchrmusum2  18573  dchrvmasumlem2  18577  dchrvmasumiflem2  18581  dchrisum0fno1  18590  rpvmasum2  18591  dchrisum0lem1  18594  dchrisum0lem2a  18595  dchrisum0lem2  18596  dchrisum0lem3  18597  dchrmusumlem  18600  rpvmasum  18604  rplogsum  18605  dirith2  18606  issubgoi  18800  sspval  19122  ajfval  19210  shex  19614  chex  19629  hmopex  20278  kur14lem7  20907  kur14lem9  20909  dfon2lem7  21307  colinearex  21852  prodex  22413  isrocatset  23072  heibor1lem  23600  rrnval  23618  eldiophb  23906  pellexlem3  23983  pellexlem5  23985  setindtr  24184  aannenlem3  24273  cnmsgngrp  24546  onfrALTlem3VD  25200  bnj20  25574  bnj53  26353  lsatset  26823  lcvfbr  26853  cmtfvalN  27043  cvrfval  27101  lineset  27570  psubspset  27576  psubclsetN  27768  lautset  27914  pautsetN  27930  tendoset  28591  dicval  29009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-sep 3699
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1445  df-sb 1734  df-clab 2050  df-cleq 2055  df-clel 2058  df-v 2475  df-in 2798  df-ss 2802
Copyright terms: Public domain