Theorem isseti 2608

Description: A way to say " A is a set" (inference rule). (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 2606	. 2 |- ( A e. _V <-> E. x x = A )
3	1, 2	mpbi 143	1 |- E. x x = A

Syntax hints:   = wceq 1285   E.wex 1422   e. wcel 1434   _Vcvv 2602

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604

This theorem is referenced by:  rexcom4b  2625  ceqsex  2638  vtoclf  2653  vtocl2  2655  vtocl3  2656  vtoclef  2672  eqvinc  2719  euind  2780  opabm  4043  eusv2nf  4214  dtruex  4310  limom  4362  isarep2  5017  dfoprab2  5583  rnoprab  5618  dmaddpq  6631  dmmulpq  6632  bj-inf2vnlem1  10950