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

Theorem ssex 4055
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4038 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
ssex.1  |-  B  e. 
_V
Assertion
Ref Expression
ssex  |-  ( A 
C_  B  ->  A  e.  _V )

Proof of Theorem ssex
StepHypRef Expression
1 df-ss 3089 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4053 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2313 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 204 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 189 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2727    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  ssexi  4056  ssexg  4057  intex  4065  moabex  4126  ixpiunwdom  7189  omex  7228  tcss  7313  bndrank  7397  scottex  7439  aceq3lem  7631  cfslb  7776  dcomex  7957  axdc2lem  7958  grothpw  8328  grothpwex  8329  grothomex  8331  elnp  8491  hashfacen  11269  limsuple  11829  limsuplt  11830  limsupbnd1  11833  o1add2  11974  o1mul2  11975  o1sub2  11976  o1dif  11980  caucvgrlem  12022  fsumo1  12147  unbenlem  12829  ressbas2  13073  prdsval  13229  prdsbas  13231  rescbas  13550  reschom  13551  rescco  13553  issubmnd  14236  eqgfval  14500  dfod2  14712  ablfac1b  15140  2basgen  16560  prdstopn  17154  rectbntr0  18169  elcncf  18225  cncfcnvcn  18256  cmsss  18604  ovolctb2  18683  limcfval  19054  ellimc2  19059  limcflf  19063  limcres  19068  limcun  19077  dvfval  19079  lhop2  19194  taylfval  19570  ulmval  19591  xrlimcnp  20095  brsset  23604  supnuf  24795  supexr  24797  vtarsuelt  25061  isfne4  25435  refssfne  25460  topjoin  25480  filbcmb  25598  cnpwstotbnd  25687  ismtyval  25690  isnumbasgrplem2  26435  islinds2  26449  bnj849  27646  ispsubsp  28735  ispsubclN  28927
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator