Theorem isseti 3099

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

Syntax hints:   = wceq 1381   E.wex 1597   e. wcel 1802   _Vcvv 3093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095

This theorem is referenced by:  rexcom4b  3115  ceqsex  3129  vtoclf  3144  vtocl2  3146  vtocl3  3147  vtoclef  3166  eqvinc  3210  euind  3270  eusv2nf  4631  zfpair  4670  axpr  4671  opabn0  4764  isarep2  5654  dfoprab2  6324  rnoprab  6366  ov3  6420  omeu  7232  cflem  8624  genpass  9385  supmul1  10509  supmullem2  10511  supmul  10512  uzindOLD  10958  ruclem13  13847  joindm  15502  meetdm  15516  supaddc  30009  supadd  30010  ac6s6f  30549  funressnfv  32047  bnj986  33719  bj-snsetex  34233