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

Theorem ssex 4281
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 4264 (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 3270 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4279 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2440 . . 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 2892    i^i cin 3255    C_ wss 3256
This theorem is referenced by:  ssexi  4282  ssexg  4283  intex  4290  moabex  4356  ixpiunwdom  7485  omex  7524  tcss  7609  bndrank  7693  scottex  7735  aceq3lem  7927  cfslb  8072  dcomex  8253  axdc2lem  8254  grothpw  8627  grothpwex  8628  grothomex  8630  elnp  8790  hashfacen  11623  limsuple  12192  limsuplt  12193  limsupbnd1  12196  o1add2  12337  o1mul2  12338  o1sub2  12339  o1dif  12343  caucvgrlem  12386  fsumo1  12511  unbenlem  13196  ressbas2  13440  prdsval  13598  prdsbas  13600  rescbas  13949  reschom  13950  rescco  13952  acsmapd  14524  issubmnd  14644  eqgfval  14908  dfod2  15120  ablfac1b  15548  2basgen  16971  prdstopn  17574  ressust  18208  rectbntr0  18727  elcncf  18783  cncfcnvcn  18815  cmsss  19165  ovolctb2  19248  limcfval  19619  ellimc2  19624  limcflf  19628  limcres  19633  limcun  19642  dvfval  19644  lhop2  19759  taylfval  20135  ulmval  20156  xrlimcnp  20667  ressnm  24016  brsset  25446  isfne4  26033  refssfne  26058  topjoin  26078  filbcmb  26126  cnpwstotbnd  26190  ismtyval  26193  isnumbasgrplem2  26931  islinds2  26945  bnj849  28627  ispsubsp  29910  ispsubclN  30102
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 2361  ax-sep 4264
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator