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

Theorem ssex 4568
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 4546 (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 3450 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4566 . . 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 214 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 198 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   _Vcvv 3080    i^i cin 3435    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450
This theorem is referenced by:  ssexi  4569  ssexg  4570  intex  4580  moabex  4680  ixpiunwdom  8116  omex  8158  tcss  8237  bndrank  8321  scottex  8365  aceq3lem  8559  cfslb  8704  dcomex  8885  axdc2lem  8886  grothpw  9259  grothpwex  9260  grothomex  9262  elnp  9420  negfi  10562  hashfacen  12622  limsuple  13536  limsupleOLD  13537  limsuplt  13538  limsupltOLD  13539  limsupbnd1  13544  limsupbnd1OLD  13545  o1add2  13687  o1mul2  13688  o1sub2  13689  o1dif  13693  caucvgrlem  13736  caucvgrlemOLD  13737  fsumo1  13872  lcmfval  14591  lcmf0val  14592  lcmfvalOLD  14595  unbenlem  14852  ressbas2  15180  prdsval  15353  prdsbas  15355  rescbas  15734  reschom  15735  rescco  15737  acsmapd  16424  issubmnd  16564  eqgfval  16865  dfod2  17215  ablfac1b  17703  islinds2  19370  pmatcollpw3lem  19806  2basgen  20005  prdstopn  20642  ressust  21278  rectbntr0  21849  elcncf  21920  cncfcnvcn  21952  cmsss  22317  ovolctb2  22444  limcfval  22826  ellimc2  22831  limcflf  22835  limcres  22840  limcun  22849  dvfval  22851  lhop2  22966  taylfval  23313  ulmval  23334  xrlimcnp  23893  axtgcont1  24515  fpwrelmap  28325  ressnm  28420  ressprs  28424  ordtrestNEW  28736  ddeval1  29066  ddeval0  29067  bnj849  29745  msrval  30185  mclsval  30210  brsset  30662  isfne4  31002  refssfne  31020  topjoin  31027  bj-snglex  31536  mblfinlem3  31944  filbcmb  32032  cnpwstotbnd  32094  ismtyval  32097  ispsubsp  33280  ispsubclN  33472  isnumbasgrplem2  35934  rtrclex  36195  brmptiunrelexpd  36246  iunrelexp0  36265  mulcncff  37686  subcncff  37698  addcncff  37703  cncfuni  37705  divcncff  37710  etransclem1  38041  etransclem4  38044  etransclem13  38053  issubmgm2  39439  linccl  39858  ellcoellss  39879  elbigolo1  40019
  Copyright terms: Public domain W3C validator