Theorem isseti 1811

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

Syntax hints:   = wceq 954   e. wcel 956  E.wex 978  Vcvv 1807

This theorem is referenced by:  ceqsex 1830  vtoclf 1837  vtocl2 1839  vtocl3 1840  vtoclef 1853  csbie2t 2029  zfpair 2772  axpr 2773  ssopab2 2817  opabn0 2819  funfvop 3794  iinon 3901  dfoprab2 3982  rnoprab 3995  2ndconst 4087  cflem 4885  genpdm 5085  genpn0 5086  genpass 5092  reclem3pr 5138  elreal 5230  nn1suc 5895  uzindOLD 6164  infcvglem1 7164

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain