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

Theorem isseti 3488
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 2813 . 2 (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
31, 2ax-mp 5 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wex 1781  wcel 2106  Vcvv 3473
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 1913  ax-6 1971  ax-7 2011  ax-8 2108
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2809
This theorem is referenced by:  rexcom4b  3502  ceqsal  3507  ceqsalv  3509  ceqsexOLD  3521  ceqsexvOLD  3523  vtoclef  3543  vtoclfOLD  3545  vtocl  3546  euind  3716  eusv2nf  5386  zfpair  5412  axprALT  5413  opabn0  5546  isarep2  6628  dfoprab2  7451  rnoprab  7496  ov3  7553  omeu  8568  cflem  10223  genpass  10986  supaddc  12163  supadd  12164  supmul1  12165  supmullem2  12167  supmul  12168  ruclem13  16167  joindm  18310  meetdm  18324  dmscut  27238  bnj986  33795  satfdm  34189  fmla0  34202  fmlasuc0  34204  bj-snsetex  35646  bj-restn0  35773  bj-restuni  35780  ac6s6f  36844  tfsconcatlem  41855  elintima  42173  natlocalincr  45361  tworepnotupword  45371  funressnfv  45523  elpglem2  47403
  Copyright terms: Public domain W3C validator