Theorem isset 2296

Description: Two ways to say "A is a set": A class A is a member of the universal class _V (see df-v 2294) 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 3794. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 3795, 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."

Note that a constant is considered distinct from all variables. This is why _V is not included in the distinct variable list, even though df-clel 1880 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.)

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 1880	. 2 |- (A e. _V <-> E.x(x = A /\ x e. _V))
2		visset 2295	. . . 4 |- x e. _V
3	2	biantru 793	. . 3 |- (x = A <-> (x = A /\ x e. _V))
4	3	exbii 1398	. 2 |- (E.x x = A <-> E.x(x = A /\ x e. _V))
5	1, 4	bitr4i 193	1 |- (A e. _V <-> E.x x = A)

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292

This theorem is referenced by:  isseti 2297  issetri 2298  elisset 2299  elissetOLD 2300  elex 2302  vtoclgf 2345  cla4gf 2361  cla4gfOLD 2363  ceqex 2391  eueq 2427  moeq 2431  ru 2451  elrabsf 2486  snprc 3092  0ex 3446  vprc 3449  vnex 3451  pwex 3487  dmsnop 4367  dmsnopOLD 4368  funimaexg 4495  isarep2 4499  fopab2 4796  iotaex 5099  tz9.12lem1 5770  tz9.12lem3 5772  fiuni 10219  fsubbas 10281  fopab2g 14485  inficlALT 15372  ceqsex3OLD 16249  iotaexeu 16382  elnev 16404  isseta 16405

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