Theorem isseti 2780

Description: A way to say " A is a set" (inference form). (Contributed by NM, 5-Aug-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 2778	. 2 |- ( A e. _V <-> E. x x = A )
3	1, 2	mpbi 145	1 |- E. x x = A

Syntax hints:   = wceq 1373   E.wex 1515   e. wcel 2176   _Vcvv 2772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  rexcom4b  2797  ceqsex  2810  ceqsexv2d  2812  vtoclf  2826  vtocl2  2828  vtocl3  2829  vtoclef  2846  eqvinc  2896  euind  2960  opabm  4328  eusv2nf  4504  dtruex  4608  limom  4663  isarep2  5362  dfoprab2  5994  rnoprab  6030  dmaddpq  7494  dmmulpq  7495  bj-inf2vnlem1  15943