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

Theorem ssex 5319
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 5294 (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 dfss2 3968 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 ssex.1 . . . 4 𝐵 ∈ V
32inex2 5316 . . 3 (𝐴𝐵) ∈ V
4 eleq1 2828 . . 3 ((𝐴𝐵) = 𝐴 → ((𝐴𝐵) ∈ V ↔ 𝐴 ∈ V))
53, 4mpbii 233 . 2 ((𝐴𝐵) = 𝐴𝐴 ∈ V)
61, 5sylbi 217 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  Vcvv 3479  cin 3949  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-in 3957  df-ss 3967
This theorem is referenced by:  ssexi  5320  ssexg  5321  intex  5342  moabex  5462  naddunif  8727  ixpiunwdom  9626  omex  9679  tcss  9780  bndrank  9877  scottex  9921  aceq3lem  10156  cfslb  10302  dcomex  10483  axdc2lem  10484  grothpw  10862  grothpwex  10863  grothomex  10865  elnp  11023  negfi  12213  limsuple  15510  limsuplt  15511  limsupbnd1  15514  o1add2  15656  o1mul2  15657  o1sub2  15658  o1dif  15662  caucvgrlem  15705  fsumo1  15844  lcmfval  16654  lcmf0val  16655  unbenlem  16942  ressbas2  17279  prdsval  17496  prdsbas  17498  rescbas  17869  reschom  17870  rescco  17872  acsmapd  18595  issstrmgm  18662  issubmgm2  18712  issubmnd  18770  eqgfval  19190  dfod2  19578  ablfac1b  20086  islinds2  21825  pmatcollpw3lem  22779  2basgen  22987  prdstopn  23626  ressust  24262  rectbntr0  24844  elcncf  24905  cncfcnvcn  24942  cmssmscld  25374  cmsss  25375  ovolctb2  25517  limcfval  25897  ellimc2  25902  limcflf  25906  limcres  25911  limcun  25920  dvfval  25922  lhop2  26044  taylfval  26390  ulmval  26413  xrlimcnp  27001  axtgcont1  28466  fpwrelmap  32733  ressnm  32936  ressprs  32941  ordtrestNEW  33898  ddeval1  34213  ddeval0  34214  carsgclctunlem3  34300  bnj849  34917  msrval  35521  mclsval  35546  brsset  35868  isfne4  36319  refssfne  36337  topjoin  36344  bj-snglex  36952  mblfinlem3  37644  filbcmb  37725  cnpwstotbnd  37782  ismtyval  37785  ispsubsp  39725  ispsubclN  39917  isnumbasgrplem2  43094  rtrclex  43608  brmptiunrelexpd  43674  iunrelexp0  43693  mulcncff  45861  subcncff  45871  addcncff  45875  cncfuni  45877  divcncff  45882  etransclem1  46226  etransclem4  46229  etransclem13  46238  isvonmbl  46629  isubgriedg  47825  isubgrvtx  47829  uhgrimisgrgric  47875  linccl  48307  ellcoellss  48328  elbigolo1  48454
  Copyright terms: Public domain W3C validator