Theorem isseti 1352

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(s):   x,A

Proof of Theorem isseti

Step	Hyp	Ref	Expression
1		isseti.1	. 2 |- A e. V
2		isset 1351	. 2 |- (A e. V <-> E.x x = A)
3	1, 2	mpbi 164	1 |- E.x x = A

Syntax hints:  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  ceqsex 1370  vtoclf 1377  vtocl2 1379  vtocl3 1380  vtoclef 1392  zfpair 1891  ssopab2 2119  funopfv 2886  iinon 2948  dfoprab2 3021  rnoprab 3033  ac6lem 3575  cflem 3700  genpdm 3899  genpn0 3900  genpass 3906  reclem3pr 3952  elreal 4044  nn1suc 4435  uzind 4603

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org