Theorem isset 1814

Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1812) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A e. V" to mean "A is a set" very frequently, for example in uniex 2870. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 2871, in order to shorten certain proofs we use the more general antecedent A e. B instead of A e. V to mean "A is a set."

Assertion

Ref	Expression
isset	|- (A e. V <-> E.x x = A)

Distinct variable group:   x,A

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 1472	. 2 |- (A e. V <-> E.x(x = A /\ x e. V))
2		visset 1813	. . . 4 |- x e. V
3	2	biantru 724	. . 3 |- (x = A <-> (x = A /\ x e. V))
4	3	exbii 1051	. 2 |- (E.x x = A <-> E.x(x = A /\ x e. V))
5	1, 4	bitr4 176	1 |- (A e. V <-> E.x x = A)

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  Vcvv 1811

This theorem is referenced by:  isseti 1815  issetri 1816  elisset 1817  elex 1819  vtoclgf 1846  cla4gf 1860  ceqex 1886  eueq 1916  moeq 1920  ru 1938  elrabsf 1963  snprc 2443  nvelv 2713  vnex 2715  dmsnop 3328  funimaexg 3575  isarep2 3578  fopab2 3823  tz9.12lem1 4659  tz9.12lem3 4661

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