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

Theorem ssex 4288
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 4271 (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 3277 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4286 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2447 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 203 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 188 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   _Vcvv 2899    i^i cin 3262    C_ wss 3263
This theorem is referenced by:  ssexi  4289  ssexg  4290  intex  4297  moabex  4363  ixpiunwdom  7492  omex  7531  tcss  7616  bndrank  7700  scottex  7742  aceq3lem  7934  cfslb  8079  dcomex  8260  axdc2lem  8261  grothpw  8634  grothpwex  8635  grothomex  8637  elnp  8797  hashfacen  11630  limsuple  12199  limsuplt  12200  limsupbnd1  12203  o1add2  12344  o1mul2  12345  o1sub2  12346  o1dif  12350  caucvgrlem  12393  fsumo1  12518  unbenlem  13203  ressbas2  13447  prdsval  13605  prdsbas  13607  rescbas  13956  reschom  13957  rescco  13959  acsmapd  14531  issubmnd  14651  eqgfval  14915  dfod2  15127  ablfac1b  15555  2basgen  16978  prdstopn  17581  ressust  18215  rectbntr0  18734  elcncf  18790  cncfcnvcn  18822  cmsss  19172  ovolctb2  19255  limcfval  19626  ellimc2  19631  limcflf  19635  limcres  19640  limcun  19649  dvfval  19651  lhop2  19766  taylfval  20142  ulmval  20163  xrlimcnp  20674  ressnm  24023  brsset  25453  isfne4  26040  refssfne  26065  topjoin  26085  filbcmb  26133  cnpwstotbnd  26197  ismtyval  26200  isnumbasgrplem2  26938  islinds2  26952  bnj849  28634  ispsubsp  29859  ispsubclN  30051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator