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

Theorem ssex 4132
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 4115 (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 3141 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4130 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2318 . . 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 2763    i^i cin 3126    C_ wss 3127
This theorem is referenced by:  ssexi  4133  ssexg  4134  intex  4143  moabex  4204  ixpiunwdom  7273  omex  7312  tcss  7397  bndrank  7481  scottex  7523  aceq3lem  7715  cfslb  7860  dcomex  8041  axdc2lem  8042  grothpw  8416  grothpwex  8417  grothomex  8419  elnp  8579  hashfacen  11358  limsuple  11918  limsuplt  11919  limsupbnd1  11922  o1add2  12063  o1mul2  12064  o1sub2  12065  o1dif  12069  caucvgrlem  12111  fsumo1  12236  unbenlem  12918  ressbas2  13162  prdsval  13318  prdsbas  13320  rescbas  13669  reschom  13670  rescco  13672  acsmapd  14244  issubmnd  14364  eqgfval  14628  dfod2  14840  ablfac1b  15268  2basgen  16691  prdstopn  17285  rectbntr0  18300  elcncf  18356  cncfcnvcn  18387  cmsss  18735  ovolctb2  18814  limcfval  19185  ellimc2  19190  limcflf  19194  limcres  19199  limcun  19208  dvfval  19210  lhop2  19325  taylfval  19701  ulmval  19722  xrlimcnp  20226  ballotlemelo  23008  brsset  23806  supnuf  24997  supexr  24999  vtarsuelt  25263  isfne4  25637  refssfne  25662  topjoin  25682  filbcmb  25800  cnpwstotbnd  25889  ismtyval  25892  isnumbasgrplem2  26637  islinds2  26651  climdivf  27107  bnj849  28089  ispsubsp  29184  ispsubclN  29376
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 1927  ax-ext 2239  ax-sep 4115
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator