Theorem isseti 1818

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

Syntax hints:   = wceq 958   e. wcel 960  E.wex 982  Vcvv 1814

This theorem is referenced by:  ceqsex 1837  vtoclf 1844  vtocl2 1846  vtocl3 1847  vtoclef 1860  csbie2t 2036  zfpair 2783  axpr 2784  ssopab2 2828  opabn0 2830  funfvop 3809  iinon 3916  dfoprab2 3997  rnoprab 4010  2ndconst 4103  cflem 4917  genpdm 5117  genpn0 5118  genpass 5124  reclem3pr 5170  elreal 5262  nn1suc 5941  uzindOLD 6210  infcvglem1 7221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815

Copyright terms: Public domain