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

Theorem ssex 4339
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 4322 (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 3326 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4337 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2495 . . 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 1652    e. wcel 1725   _Vcvv 2948    i^i cin 3311    C_ wss 3312
This theorem is referenced by:  ssexi  4340  ssexg  4341  intex  4348  moabex  4414  ixpiunwdom  7548  omex  7587  tcss  7672  bndrank  7756  scottex  7798  aceq3lem  7990  cfslb  8135  dcomex  8316  axdc2lem  8317  grothpw  8690  grothpwex  8691  grothomex  8693  elnp  8853  hashfacen  11691  limsuple  12260  limsuplt  12261  limsupbnd1  12264  o1add2  12405  o1mul2  12406  o1sub2  12407  o1dif  12411  caucvgrlem  12454  fsumo1  12579  unbenlem  13264  ressbas2  13508  prdsval  13666  prdsbas  13668  rescbas  14017  reschom  14018  rescco  14020  acsmapd  14592  issubmnd  14712  eqgfval  14976  dfod2  15188  ablfac1b  15616  2basgen  17043  prdstopn  17648  ressust  18282  rectbntr0  18851  elcncf  18907  cncfcnvcn  18939  cmsss  19291  ovolctb2  19376  limcfval  19747  ellimc2  19752  limcflf  19756  limcres  19761  limcun  19770  dvfval  19772  lhop2  19887  taylfval  20263  ulmval  20284  xrlimcnp  20795  ressnm  24172  brsset  25684  mblfinlem2  26191  isfne4  26286  refssfne  26311  topjoin  26331  filbcmb  26379  cnpwstotbnd  26443  ismtyval  26446  isnumbasgrplem2  27184  islinds2  27198  bnj849  29150  ispsubsp  30381  ispsubclN  30573
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator