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

Theorem ssex 5211
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 5189 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
ssex.1 𝐵 ∈ V
Assertion
Ref Expression
ssex (𝐴𝐵𝐴 ∈ V)

Proof of Theorem ssex
StepHypRef Expression
1 df-ss 3936 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 ssex.1 . . . 4 𝐵 ∈ V
32inex2 5208 . . 3 (𝐴𝐵) ∈ V
4 eleq1 2903 . . 3 ((𝐴𝐵) = 𝐴 → ((𝐴𝐵) ∈ V ↔ 𝐴 ∈ V))
53, 4mpbii 236 . 2 ((𝐴𝐵) = 𝐴𝐴 ∈ V)
61, 5sylbi 220 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3480  cin 3918  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5189
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  ssexi  5212  ssexg  5213  intex  5226  moabex  5338  ixpiunwdom  9051  omex  9103  tcss  9183  bndrank  9267  scottex  9311  aceq3lem  9544  cfslb  9686  dcomex  9867  axdc2lem  9868  grothpw  10246  grothpwex  10247  grothomex  10249  elnp  10407  negfi  11586  hashfacen  13817  limsuple  14835  limsuplt  14836  limsupbnd1  14839  o1add2  14980  o1mul2  14981  o1sub2  14982  o1dif  14986  caucvgrlem  15029  fsumo1  15167  lcmfval  15963  lcmf0val  15964  unbenlem  16242  ressbas2  16555  prdsval  16728  prdsbas  16730  rescbas  17099  reschom  17100  rescco  17102  acsmapd  17788  issstrmgm  17863  issubmnd  17938  eqgfval  18328  dfod2  18691  ablfac1b  19192  islinds2  20559  pmatcollpw3lem  21394  2basgen  21601  prdstopn  22239  ressust  22876  rectbntr0  23443  elcncf  23500  cncfcnvcn  23536  cmssmscld  23960  cmsss  23961  ovolctb2  24102  limcfval  24481  ellimc2  24486  limcflf  24490  limcres  24495  limcun  24504  dvfval  24506  lhop2  24624  taylfval  24960  ulmval  24981  xrlimcnp  25560  axtgcont1  26268  fpwrelmap  30483  ressnm  30652  ressprs  30656  ordtrestNEW  31224  ddeval1  31553  ddeval0  31554  carsgclctunlem3  31638  bnj849  32257  msrval  32845  mclsval  32870  brsset  33410  isfne4  33748  refssfne  33766  topjoin  33773  bj-snglex  34356  mblfinlem3  35044  filbcmb  35126  cnpwstotbnd  35183  ismtyval  35186  ispsubsp  36989  ispsubclN  37181  isnumbasgrplem2  39968  rtrclex  40237  brmptiunrelexpd  40304  iunrelexp0  40323  mulcncff  42442  subcncff  42452  addcncff  42456  cncfuni  42458  divcncff  42463  etransclem1  42807  etransclem4  42810  etransclem13  42819  isvonmbl  43207  issubmgm2  44340  linccl  44753  ellcoellss  44774  elbigolo1  44901
  Copyright terms: Public domain W3C validator