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

Theorem ssex 5282
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 5260 (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 3931 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 ssex.1 . . . 4 𝐵 ∈ V
32inex2 5279 . . 3 (𝐴𝐵) ∈ V
4 eleq1 2822 . . 3 ((𝐴𝐵) = 𝐴 → ((𝐴𝐵) ∈ V ↔ 𝐴 ∈ V))
53, 4mpbii 232 . 2 ((𝐴𝐵) = 𝐴𝐴 ∈ V)
61, 5sylbi 216 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3447  cin 3913  wss 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-in 3921  df-ss 3931
This theorem is referenced by:  ssexi  5283  ssexg  5284  intex  5298  moabex  5420  naddunif  8643  ixpiunwdom  9534  omex  9587  tcss  9688  bndrank  9785  scottex  9829  aceq3lem  10064  cfslb  10210  dcomex  10391  axdc2lem  10392  grothpw  10770  grothpwex  10771  grothomex  10773  elnp  10931  negfi  12112  hashfacenOLD  14361  limsuple  15369  limsuplt  15370  limsupbnd1  15373  o1add2  15515  o1mul2  15516  o1sub2  15517  o1dif  15521  caucvgrlem  15566  fsumo1  15705  lcmfval  16505  lcmf0val  16506  unbenlem  16788  ressbas2  17128  prdsval  17345  prdsbas  17347  rescbas  17720  rescbasOLD  17721  reschom  17722  rescco  17724  resccoOLD  17725  acsmapd  18451  issstrmgm  18516  issubmnd  18591  eqgfval  18986  dfod2  19354  ablfac1b  19857  islinds2  21242  pmatcollpw3lem  22155  2basgen  22363  prdstopn  23002  ressust  23638  rectbntr0  24218  elcncf  24275  cncfcnvcn  24311  cmssmscld  24737  cmsss  24738  ovolctb2  24879  limcfval  25259  ellimc2  25264  limcflf  25268  limcres  25273  limcun  25282  dvfval  25284  lhop2  25402  taylfval  25741  ulmval  25762  xrlimcnp  26341  axtgcont1  27459  fpwrelmap  31704  ressnm  31874  ressprs  31879  ordtrestNEW  32566  ddeval1  32897  ddeval0  32898  carsgclctunlem3  32984  bnj849  33601  msrval  34196  mclsval  34221  brsset  34527  isfne4  34865  refssfne  34883  topjoin  34890  bj-snglex  35494  mblfinlem3  36167  filbcmb  36249  cnpwstotbnd  36306  ismtyval  36309  ispsubsp  38258  ispsubclN  38450  isnumbasgrplem2  41478  rtrclex  41981  brmptiunrelexpd  42047  iunrelexp0  42066  mulcncff  44201  subcncff  44211  addcncff  44215  cncfuni  44217  divcncff  44222  etransclem1  44566  etransclem4  44569  etransclem13  44578  isvonmbl  44969  issubmgm2  46174  linccl  46585  ellcoellss  46606  elbigolo1  46733
  Copyright terms: Public domain W3C validator