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

Theorem ssex 4591
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 4568 (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 3490 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4589 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2539 . . 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 1379    e. wcel 1767   _Vcvv 3113    i^i cin 3475    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  ssexi  4592  ssexg  4593  intex  4603  moabex  4706  ixpiunwdom  8017  omex  8060  tcss  8175  bndrank  8259  scottex  8303  aceq3lem  8501  cfslb  8646  dcomex  8827  axdc2lem  8828  grothpw  9204  grothpwex  9205  grothomex  9207  elnp  9365  hashfacen  12469  limsuple  13264  limsuplt  13265  limsupbnd1  13268  o1add2  13409  o1mul2  13410  o1sub2  13411  o1dif  13415  caucvgrlem  13458  fsumo1  13589  unbenlem  14285  ressbas2  14546  prdsval  14710  prdsbas  14712  rescbas  15059  reschom  15060  rescco  15062  acsmapd  15665  issubmnd  15767  eqgfval  16054  dfod2  16392  ablfac1b  16923  islinds2  18643  pmatcollpw3lem  19079  2basgen  19286  prdstopn  19892  ressust  20530  rectbntr0  21100  elcncf  21156  cncfcnvcn  21188  cmsss  21552  ovolctb2  21666  limcfval  22039  ellimc2  22044  limcflf  22048  limcres  22053  limcun  22062  dvfval  22064  lhop2  22179  taylfval  22516  ulmval  22537  xrlimcnp  23054  axtgcont1  23621  fpwrelmap  27256  ressnm  27329  ressprs  27333  ordtrestNEW  27567  ddeval1  27874  ddeval0  27875  eulerpartlem1  27974  brsset  29144  mblfinlem3  29658  isfne4  29769  refssfne  29794  topjoin  29814  filbcmb  29862  cnpwstotbnd  29924  ismtyval  29927  isnumbasgrplem2  30685  mulcncff  31234  subcncff  31246  addcncff  31251  cncfuni  31253  divcncff  31258  linccl  32114  ellcoellss  32135  bnj849  33080  bj-snglex  33630  ispsubsp  34559  ispsubclN  34751
  Copyright terms: Public domain W3C validator