Theorem isseti 3112

Description: A way to say " A is a set" (inference rule). (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
isseti.1	|- A e. _V

Assertion

Ref	Expression
isseti	|- E. x x = A

Distinct variable group:   x, A

Proof of Theorem isseti

Step	Hyp	Ref	Expression
1		isseti.1	. 2 |- A e. _V
2		isset 3110	. 2 |- ( A e. _V <-> E. x x = A )
3	1, 2	mpbi 208	1 |- E. x x = A

Syntax hints:   = wceq 1398   E.wex 1617   e. wcel 1823   _Vcvv 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108

This theorem is referenced by:  rexcom4b  3128  ceqsex  3142  vtoclf  3157  vtocl2  3159  vtocl3  3160  vtoclef  3179  eqvinc  3223  euind  3283  eusv2nf  4635  zfpair  4674  axpr  4675  opabn0  4767  isarep2  5650  dfoprab2  6316  rnoprab  6358  ov3  6412  omeu  7226  cflem  8617  genpass  9376  supmul1  10503  supmullem2  10505  supmul  10506  uzindOLD  10953  ruclem13  14062  joindm  15835  meetdm  15849  supaddc  30284  supadd  30285  ac6s6f  30824  funressnfv  32455  bnj986  34432  bj-snsetex  34941  elintima  38198