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

Theorem ssexi 3612
Description: The subset of a set is also a set.
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 3611 . 2 |- (A C_ B -> A e. _V)
41, 3ax-mp 7 1 |- A e. _V
Colors of variables: wff set class
Syntax hints:   e. wcel 1575  _Vcvv 2482   C_ wss 2784
This theorem is referenced by:  zfausab 3615  ord3ex 3650  moabex 3678  opabex 4917  fvclex 4990  abrexexlem1 4992  abrexex 4994  oprabex 5118  oev 5505  pw2en 5824  sbthlem2 5826  phplem2 5945  phplem4 5947  php 5949  pssnn 5984  ordtypelem1 6071  ordtypelem7 6077  hartogslem 6079  inf3lem3 6110  hta 6323  aceq3 6420  aceq5lem4 6425  aceq6b 6429  domtriomlem 6535  axdc3lem 6542  axcclem 6549  numthlem 6594  zorn2lem1 6599  brdom7disj 6619  brdom6disj 6620  unidom 6623  konigthlem 6649  infmap2lem2 6670  gch-kn 6677  niex 6855  enqex 6897  npex 6961  enrex 7044  zex 8036  sumex 9154  isprm2lem 9883  strss 9951  subbas 10494  blfval 10720  bcthlem1 10898  bcthlem5 10902  issubg 11021  issubgi 11027  sspval 11312  ajfval 11400  symgval 11715  shex 12230  chex 12245  hmopex 12949  enrexNEW 13553  zexNEW 13622  dfon2lem7 14141  colinearex 14685  prodex 15363  issubcat 15974  isrocatset 16110  cptclsscpt 16328  2ndcctbss 16375  neibastop2lem1 16416  neibastop2lem4 16419  cnresoprab2 16802  heibor1lem 16842  heiborlem3 16846  phtpcval 16915  pcofval 16929  pi1bval 16945  rnghomval 16973  onfrALTlem3VD 17557  bnj20 17919  bnj53 18698  cmtfval 19130  cvrfval 19189  csubspset 19463  lineset 19719  psubspset 19725  psubclset 19918  lautset 20067  pautset 20088  tendoset 20811  l1dset 21352
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057  ax-sep 3592
This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-ex 1502  df-sb 1748  df-clab 2063  df-cleq 2068  df-clel 2071  df-v 2484  df-in 2791  df-ss 2793
Copyright terms: Public domain