Theorem isseti 1815

Description: A way to say "A is a set" (inference rule).

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 1814	. 2 |- (A e. V <-> E.x x = A)
3	1, 2	mpbi 189	1 |- E.x x = A

Syntax hints:   = wceq 956   e. wcel 958  E.wex 980  Vcvv 1811

This theorem is referenced by:  ceqsex 1834  vtoclf 1841  vtocl2 1843  vtocl3 1844  vtoclef 1857  csbie2t 2033  zfpair 2777  axpr 2778  ssopab2 2822  opabn0 2824  funfvop 3803  iinon 3910  dfoprab2 3991  rnoprab 4004  2ndconst 4097  cflem 4905  genpdm 5105  genpn0 5106  genpass 5112  reclem3pr 5158  elreal 5250  nn1suc 5939  uzindOLD 6208  infcvglem1 7221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain