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

Theorem ssexi 3488
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 3487 . 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 1451  _Vcvv 2358   C_ wss 2657
This theorem is referenced by:  zfausab 3491  ord3ex 3526  moabex 3555  opabex 4802  fvclex 4869  abrexexlem1 4871  abrexex 4873  oprabex 4999  oev 5415  sbthlem2 5765  phplem2 5881  phplem4 5883  php 5885  pssnn 5920  ordtypelem1 6022  ordtypelem7 6028  hartogslem 6030  inf3lem3 6061  hta 6232  aceq3 6328  aceq5lem4 6333  aceq6b 6337  domtriomlem 6443  axdc3lem 6450  axcclem 6457  numthlem 6502  zorn2lem1 6507  brdom7disj 6527  brdom6disj 6528  unidom 6531  konigthlem 6557  infmap2lem2 6578  gch-kn 6585  niex 6764  enqex 6806  npex 6870  enrex 6953  isprm2lem 9667  1arithlem1 9810  1arith 9814  strss 9909  issubgi 10621  symgval 10706  cmpcld 11054  hmph 11118  blfval 11247  qtopbaslem 11328  divcn 11379  evth 11411  phtpyfval 11416  phtpcval 11423  pi1bval 11451  bcthlem1 11527  bcthlem5 11531  sspval 11736  ajfval 11824  vitalilem2 12081  vitalilem3 12082  vitali 12085  itg2seq 12214  shex 13056  chex 13071  hmopex 13721  dfon2lem7 14518  colinearex 15075  prodex 15751  issubcat 16387  isrocatset 16524  2ndcctbss 16761  neibastop2lem1 16802  neibastop2lem4 16805  heibor1lem 17125  heiborlem3 17129  rngohomval 17189  onfrALTlem3VD 17831  bnj20 18195  bnj53 18974  cmtfval 19406  cvrfval 19465  lineset 19988  psubspset 19994  psubclset 20187  lautset 20337  pautset 20358  tendoset 21091
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-sep 3469
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-ex 1372  df-sb 1626  df-clab 1941  df-cleq 1946  df-clel 1949  df-v 2360  df-in 2664  df-ss 2666
Copyright terms: Public domain