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

Theorem ssex 4540
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 4518 (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 3404 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4538 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2537 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 216 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 200 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452    e. wcel 1904   _Vcvv 3031    i^i cin 3389    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404
This theorem is referenced by:  ssexi  4541  ssexg  4542  intex  4557  moabex  4659  ixpiunwdom  8124  omex  8166  tcss  8246  bndrank  8330  scottex  8374  aceq3lem  8569  cfslb  8714  dcomex  8895  axdc2lem  8896  grothpw  9269  grothpwex  9270  grothomex  9272  elnp  9430  negfi  10576  hashfacen  12658  limsuple  13613  limsupleOLD  13614  limsuplt  13615  limsupltOLD  13616  limsupbnd1  13621  limsupbnd1OLD  13622  o1add2  13764  o1mul2  13765  o1sub2  13766  o1dif  13770  caucvgrlem  13813  caucvgrlemOLD  13814  fsumo1  13949  lcmfval  14670  lcmf0val  14671  lcmfvalOLD  14674  unbenlem  14931  ressbas2  15258  prdsval  15431  prdsbas  15433  rescbas  15812  reschom  15813  rescco  15815  acsmapd  16502  issubmnd  16642  eqgfval  16943  dfod2  17293  ablfac1b  17781  islinds2  19448  pmatcollpw3lem  19884  2basgen  20083  prdstopn  20720  ressust  21357  rectbntr0  21928  elcncf  21999  cncfcnvcn  22031  cmsss  22396  ovolctb2  22523  limcfval  22906  ellimc2  22911  limcflf  22915  limcres  22920  limcun  22929  dvfval  22931  lhop2  23046  taylfval  23393  ulmval  23414  xrlimcnp  23973  axtgcont1  24595  fpwrelmap  28393  ressnm  28487  ressprs  28491  ordtrestNEW  28801  ddeval1  29130  ddeval0  29131  bnj849  29808  msrval  30248  mclsval  30273  brsset  30727  isfne4  31067  refssfne  31085  topjoin  31092  bj-snglex  31637  mblfinlem3  32043  filbcmb  32131  cnpwstotbnd  32193  ismtyval  32196  ispsubsp  33381  ispsubclN  33573  isnumbasgrplem2  36034  rtrclex  36295  brmptiunrelexpd  36346  iunrelexp0  36365  mulcncff  37842  subcncff  37854  addcncff  37859  cncfuni  37861  divcncff  37866  etransclem1  38212  etransclem4  38215  etransclem13  38224  isvonmbl  38578  issubmgm2  40298  linccl  40715  ellcoellss  40736  elbigolo1  40876
  Copyright terms: Public domain W3C validator