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

Theorem ssex 4158
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 4141 (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 3166 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4156 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2343 . . 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 1684   _Vcvv 2788    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  ssexi  4159  ssexg  4160  intex  4167  moabex  4232  ixpiunwdom  7305  omex  7344  tcss  7429  bndrank  7513  scottex  7555  aceq3lem  7747  cfslb  7892  dcomex  8073  axdc2lem  8074  grothpw  8448  grothpwex  8449  grothomex  8451  elnp  8611  hashfacen  11392  limsuple  11952  limsuplt  11953  limsupbnd1  11956  o1add2  12097  o1mul2  12098  o1sub2  12099  o1dif  12103  caucvgrlem  12145  fsumo1  12270  unbenlem  12955  ressbas2  13199  prdsval  13355  prdsbas  13357  rescbas  13706  reschom  13707  rescco  13709  acsmapd  14281  issubmnd  14401  eqgfval  14665  dfod2  14877  ablfac1b  15305  2basgen  16728  prdstopn  17322  rectbntr0  18337  elcncf  18393  cncfcnvcn  18424  cmsss  18772  ovolctb2  18851  limcfval  19222  ellimc2  19227  limcflf  19231  limcres  19236  limcun  19245  dvfval  19247  lhop2  19362  taylfval  19738  ulmval  19759  xrlimcnp  20263  ballotlemelo  23046  brsset  24429  supnuf  25629  supexr  25631  vtarsuelt  25895  isfne4  26269  refssfne  26294  topjoin  26314  filbcmb  26432  cnpwstotbnd  26521  ismtyval  26524  isnumbasgrplem2  27269  islinds2  27283  climdivf  27738  bnj849  28957  ispsubsp  29934  ispsubclN  30126
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator