MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssex Structured version   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  7551  omex  7590  tcss  7675  bndrank  7759  scottex  7801  aceq3lem  7993  cfslb  8138  dcomex  8319  axdc2lem  8320  grothpw  8693  grothpwex  8694  grothomex  8696  elnp  8856  hashfacen  11695  limsuple  12264  limsuplt  12265  limsupbnd1  12268  o1add2  12409  o1mul2  12410  o1sub2  12411  o1dif  12415  caucvgrlem  12458  fsumo1  12583  unbenlem  13268  ressbas2  13512  prdsval  13670  prdsbas  13672  rescbas  14021  reschom  14022  rescco  14024  acsmapd  14596  issubmnd  14716  eqgfval  14980  dfod2  15192  ablfac1b  15620  2basgen  17047  prdstopn  17652  ressust  18286  rectbntr0  18855  elcncf  18911  cncfcnvcn  18943  cmsss  19295  ovolctb2  19380  limcfval  19751  ellimc2  19756  limcflf  19760  limcres  19765  limcun  19774  dvfval  19776  lhop2  19891  taylfval  20267  ulmval  20288  xrlimcnp  20799  ressnm  24176  brsset  25726  mblfinlem2  26235  isfne4  26330  refssfne  26355  topjoin  26375  filbcmb  26423  cnpwstotbnd  26487  ismtyval  26490  isnumbasgrplem2  27227  islinds2  27241  bnj849  29223  ispsubsp  30469  ispsubclN  30661
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