Theorem isseti 3062

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

Syntax hints:   = wceq 1454   E.wex 1673   e. wcel 1897   _Vcvv 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058

This theorem is referenced by:  rexcom4b  3080  ceqsex  3094  vtoclf  3110  vtocl  3111  vtocl2  3113  vtocl3  3114  vtoclef  3133  eqvinc  3177  euind  3236  eusv2nf  4614  zfpair  4650  axpr  4651  opabn0  4745  isarep2  5684  dfoprab2  6363  rnoprab  6405  ov3  6459  omeu  7311  cflem  8701  genpass  9459  supaddc  10601  supadd  10602  supmul1  10603  supmullem2  10605  supmul  10606  ruclem13  14342  joindm  16297  meetdm  16311  bnj986  29813  bj-snsetex  31601  ac6s6f  32460  elintima  36289  funressnfv  38666