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

Theorem ssex 4174
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 4157 (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 3179 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4172 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2356 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 202 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 187 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   _Vcvv 2801    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  ssexi  4175  ssexg  4176  intex  4183  moabex  4248  ixpiunwdom  7321  omex  7360  tcss  7445  bndrank  7529  scottex  7571  aceq3lem  7763  cfslb  7908  dcomex  8089  axdc2lem  8090  grothpw  8464  grothpwex  8465  grothomex  8467  elnp  8627  hashfacen  11408  limsuple  11968  limsuplt  11969  limsupbnd1  11972  o1add2  12113  o1mul2  12114  o1sub2  12115  o1dif  12119  caucvgrlem  12161  fsumo1  12286  unbenlem  12971  ressbas2  13215  prdsval  13371  prdsbas  13373  rescbas  13722  reschom  13723  rescco  13725  acsmapd  14297  issubmnd  14417  eqgfval  14681  dfod2  14893  ablfac1b  15321  2basgen  16744  prdstopn  17338  rectbntr0  18353  elcncf  18409  cncfcnvcn  18440  cmsss  18788  ovolctb2  18867  limcfval  19238  ellimc2  19243  limcflf  19247  limcres  19252  limcun  19261  dvfval  19263  lhop2  19378  taylfval  19754  ulmval  19775  xrlimcnp  20279  ballotlemelo  23062  brsset  24500  supnuf  25732  supexr  25734  vtarsuelt  25998  isfne4  26372  refssfne  26397  topjoin  26417  filbcmb  26535  cnpwstotbnd  26624  ismtyval  26627  isnumbasgrplem2  27372  islinds2  27386  climdivf  27841  bnj849  29273  ispsubsp  30556  ispsubclN  30748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator