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

Theorem ssex 4160
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 4143 (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 3168 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4158 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2345 . . 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 1625    e. wcel 1686   _Vcvv 2790    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  ssexi  4161  ssexg  4162  intex  4169  moabex  4234  ixpiunwdom  7307  omex  7346  tcss  7431  bndrank  7515  scottex  7557  aceq3lem  7749  cfslb  7894  dcomex  8075  axdc2lem  8076  grothpw  8450  grothpwex  8451  grothomex  8453  elnp  8613  hashfacen  11394  limsuple  11954  limsuplt  11955  limsupbnd1  11958  o1add2  12099  o1mul2  12100  o1sub2  12101  o1dif  12105  caucvgrlem  12147  fsumo1  12272  unbenlem  12957  ressbas2  13201  prdsval  13357  prdsbas  13359  rescbas  13708  reschom  13709  rescco  13711  acsmapd  14283  issubmnd  14403  eqgfval  14667  dfod2  14879  ablfac1b  15307  2basgen  16730  prdstopn  17324  rectbntr0  18339  elcncf  18395  cncfcnvcn  18426  cmsss  18774  ovolctb2  18853  limcfval  19224  ellimc2  19229  limcflf  19233  limcres  19238  limcun  19247  dvfval  19249  lhop2  19364  taylfval  19740  ulmval  19761  xrlimcnp  20265  ballotlemelo  23048  brsset  24431  supnuf  25640  supexr  25642  vtarsuelt  25906  isfne4  26280  refssfne  26305  topjoin  26325  filbcmb  26443  cnpwstotbnd  26532  ismtyval  26535  isnumbasgrplem2  27280  islinds2  27294  climdivf  27749  bnj849  29030  ispsubsp  30007  ispsubclN  30199
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator