Theorem isseti 2297

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 2296	. 2 |- (A e. _V <-> E.x x = A)
3	1, 2	mpbi 206	1 |- E.x x = A

Syntax hints:   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292

This theorem is referenced by:  ceqsex 2324  vtoclf 2338  vtocl2 2340  vtocl2OLD 2341  vtocl3 2342  vtocl3OLD 2343  vtoclef 2358  eqvinc 2387  euind 2439  csbie2t 2578  zfpair 3522  axpr 3523  ssopab2 3573  opabn0 3575  snnex 3801  funfvop 4776  dfoprab2 4917  rnoprab 4933  iinon 5115  cflem 6053  genpdm 6257  genpn0 6258  genpass 6264  reclem3pr 6310  elreal 6402  nn1suc 7122  uzindOLD 7420  infcvglem1 8482  rexcom4b 10148  oprabopabf 10157  bnj90OLD 12446  bnj100 12449  bnj99 12450  bnj898 12815  bnj1009 12875  bnj609 13306  bnj854 13314  bnj986 13360  bnj1015 13375  dmoprabss6 14336  rexcom4bOLD 15660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain