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

Theorem ssex 4441
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 4418 (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 3347 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4439 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2503 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 211 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 195 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   _Vcvv 2977    i^i cin 3332    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347
This theorem is referenced by:  ssexi  4442  ssexg  4443  intex  4453  moabex  4556  ixpiunwdom  7811  omex  7854  tcss  7969  bndrank  8053  scottex  8097  aceq3lem  8295  cfslb  8440  dcomex  8621  axdc2lem  8622  grothpw  8998  grothpwex  8999  grothomex  9001  elnp  9161  hashfacen  12212  limsuple  12961  limsuplt  12962  limsupbnd1  12965  o1add2  13106  o1mul2  13107  o1sub2  13108  o1dif  13112  caucvgrlem  13155  fsumo1  13280  unbenlem  13974  ressbas2  14234  prdsval  14398  prdsbas  14400  rescbas  14747  reschom  14748  rescco  14750  acsmapd  15353  issubmnd  15454  eqgfval  15734  dfod2  16070  ablfac1b  16576  islinds2  18247  2basgen  18600  prdstopn  19206  ressust  19844  rectbntr0  20414  elcncf  20470  cncfcnvcn  20502  cmsss  20866  ovolctb2  20980  limcfval  21352  ellimc2  21357  limcflf  21361  limcres  21366  limcun  21375  dvfval  21377  lhop2  21492  taylfval  21829  ulmval  21850  xrlimcnp  22367  axtgcont1  22934  fpwrelmap  26038  ressnm  26117  ressprs  26121  ordtrestNEW  26356  ddeval1  26655  ddeval0  26656  eulerpartlem1  26755  brsset  27925  mblfinlem3  28435  isfne4  28546  refssfne  28571  topjoin  28591  filbcmb  28639  cnpwstotbnd  28701  ismtyval  28704  isnumbasgrplem2  29465  linccl  30953  ellcoellss  30974  bnj849  31923  bj-snglex  32471  ispsubsp  33394  ispsubclN  33586
  Copyright terms: Public domain W3C validator