Theorem isseti 3084

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

Syntax hints:   = wceq 1370   E.wex 1587   e. wcel 1758   _Vcvv 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080

This theorem is referenced by:  rexcom4b  3100  ceqsex  3114  vtoclf  3129  vtocl2  3131  vtocl3  3132  vtoclef  3151  eqvinc  3193  euind  3253  eusv2nf  4599  zfpair  4638  axpr  4639  opabn0  4728  isarep2  5607  dfoprab2  6243  rnoprab  6284  ov3  6338  omeu  7135  cflem  8527  genpass  9290  supmul1  10407  supmullem2  10409  supmul  10410  uzindOLD  10848  ruclem13  13643  joindm  15293  meetdm  15307  supaddc  28566  supadd  28567  ac6s6f  29134  funressnfv  30183  bnj986  32280  bj-snsetex  32789