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

Theorem ssex 4159
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 4142 (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 3167 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4157 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2344 . . 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 1623    e. wcel 1685   _Vcvv 2789    i^i cin 3152    C_ wss 3153
This theorem is referenced by:  ssexi  4160  ssexg  4161  intex  4170  moabex  4231  ixpiunwdom  7301  omex  7340  tcss  7425  bndrank  7509  scottex  7551  aceq3lem  7743  cfslb  7888  dcomex  8069  axdc2lem  8070  grothpw  8444  grothpwex  8445  grothomex  8447  elnp  8607  hashfacen  11388  limsuple  11948  limsuplt  11949  limsupbnd1  11952  o1add2  12093  o1mul2  12094  o1sub2  12095  o1dif  12099  caucvgrlem  12141  fsumo1  12266  unbenlem  12951  ressbas2  13195  prdsval  13351  prdsbas  13353  rescbas  13702  reschom  13703  rescco  13705  acsmapd  14277  issubmnd  14397  eqgfval  14661  dfod2  14873  ablfac1b  15301  2basgen  16724  prdstopn  17318  rectbntr0  18333  elcncf  18389  cncfcnvcn  18420  cmsss  18768  ovolctb2  18847  limcfval  19218  ellimc2  19223  limcflf  19227  limcres  19232  limcun  19241  dvfval  19243  lhop2  19358  taylfval  19734  ulmval  19755  xrlimcnp  20259  ballotlemelo  23042  brsset  23840  supnuf  25040  supexr  25042  vtarsuelt  25306  isfne4  25680  refssfne  25705  topjoin  25725  filbcmb  25843  cnpwstotbnd  25932  ismtyval  25935  isnumbasgrplem2  26680  islinds2  26694  climdivf  27149  bnj849  28236  ispsubsp  29213  ispsubclN  29405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator