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

Theorem ssex 4596
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 4573 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
ssex.1
Assertion
Ref Expression
ssex

Proof of Theorem ssex
StepHypRef Expression
1 df-ss 3489 . 2
2 ssex.1 . . . 4
32inex2 4594 . . 3
4 eleq1 2529 . . 3
53, 4mpbii 211 . 2
61, 5sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  i^icin 3474  C_wss 3475
This theorem is referenced by:  ssexi  4597  ssexg  4598  intex  4608  moabex  4711  ixpiunwdom  8038  omex  8081  tcss  8196  bndrank  8280  scottex  8324  aceq3lem  8522  cfslb  8667  dcomex  8848  axdc2lem  8849  grothpw  9225  grothpwex  9226  grothomex  9228  elnp  9386  hashfacen  12503  limsuple  13301  limsuplt  13302  limsupbnd1  13305  o1add2  13446  o1mul2  13447  o1sub2  13448  o1dif  13452  caucvgrlem  13495  fsumo1  13626  unbenlem  14426  ressbas2  14688  prdsval  14852  prdsbas  14854  rescbas  15198  reschom  15199  rescco  15201  acsmapd  15808  issubmnd  15948  eqgfval  16249  dfod2  16586  ablfac1b  17121  islinds2  18848  pmatcollpw3lem  19284  2basgen  19492  prdstopn  20129  ressust  20767  rectbntr0  21337  elcncf  21393  cncfcnvcn  21425  cmsss  21789  ovolctb2  21903  limcfval  22276  ellimc2  22281  limcflf  22285  limcres  22290  limcun  22299  dvfval  22301  lhop2  22416  taylfval  22754  ulmval  22775  xrlimcnp  23298  axtgcont1  23865  fpwrelmap  27556  ressnm  27639  ressprs  27643  ordtrestNEW  27903  ddeval1  28206  ddeval0  28207  msrval  28898  mclsval  28923  brsset  29539  mblfinlem3  30053  isfne4  30158  refssfne  30176  topjoin  30183  filbcmb  30231  cnpwstotbnd  30293  ismtyval  30296  isnumbasgrplem2  31053  mulcncff  31670  subcncff  31682  addcncff  31687  cncfuni  31689  divcncff  31694  etransclem1  32018  etransclem4  32021  etransclem13  32030  issubmgm2  32478  linccl  33015  ellcoellss  33036  bnj849  33983  bj-snglex  34531  ispsubsp  35469  ispsubclN  35661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator