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

Theorem isseti 3498
Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.)
Hypothesis
Ref Expression
isseti.1 𝐴 ∈ V
Assertion
Ref Expression
isseti 𝑥 𝑥 = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2 𝐴 ∈ V
2 elissetv 2822 . 2 (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
31, 2ax-mp 5 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480
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
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816
This theorem is referenced by:  rexcom4b  3513  ceqsal  3519  ceqsalv  3521  ceqsexOLD  3531  ceqsexv2d  3533  vtocle  3555  vtoclOLD  3559  vtoclef  3563  vtoclfOLD  3565  euind  3730  eusv2nf  5395  zfpair  5421  axprALT  5422  opabn0  5558  isarep2  6658  dfoprab2  7491  rnoprab  7538  ov3  7596  omeu  8623  cflem  10285  cflemOLD  10286  genpass  11049  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  ruclem13  16278  joindm  18420  meetdm  18434  dmscut  27856  bnj986  34969  satfdm  35374  fmla0  35387  fmlasuc0  35389  bj-snsetex  36964  bj-restn0  37091  bj-restuni  37098  ac6s6f  38180  tfsconcatlem  43349  elintima  43666  ormklocald  46889  natlocalincr  46891  tworepnotupword  46901  funressnfv  47055  elpglem2  49231
  Copyright terms: Public domain W3C validator