Theorem isseti 3028

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 3026	. 2 |- ( A e. _V <-> E. x x = A )
3	1, 2	mpbi 211	1 |- E. x x = A

Syntax hints:   = wceq 1437   E.wex 1657   e. wcel 1872   _Vcvv 3022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3024

This theorem is referenced by:  rexcom4b  3045  ceqsex  3059  vtoclf  3074  vtocl  3075  vtocl2  3077  vtocl3  3078  vtoclef  3097  eqvinc  3141  euind  3200  eusv2nf  4565  zfpair  4601  axpr  4602  opabn0  4694  isarep2  5624  dfoprab2  6295  rnoprab  6337  ov3  6391  omeu  7241  cflem  8627  genpass  9385  supaddc  10525  supadd  10526  supmul1  10527  supmullem2  10529  supmul  10530  ruclem13  14237  joindm  16192  meetdm  16206  bnj986  29717  bj-snsetex  31468  ac6s6f  32323  elintima  36158  funressnfv  38443