Theorem isseti 2785

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

Syntax hints:   = wceq 1373   E.wex 1516   e. wcel 2178   _Vcvv 2776

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  rexcom4b  2802  ceqsex  2815  ceqsexv2d  2817  vtoclf  2831  vtocl2  2833  vtocl3  2834  vtoclef  2853  eqvinc  2903  euind  2967  opabm  4345  eusv2nf  4521  dtruex  4625  limom  4680  isarep2  5380  dfoprab2  6015  rnoprab  6051  dmaddpq  7527  dmmulpq  7528  bj-inf2vnlem1  16105