HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem isset 1789
Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1787) 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 2834. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 2835, 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
StepHypRef Expression
1 df-clel 1449 . 2 |- (A e. V <-> E.x(x = A /\ x e. V))
2 visset 1788 . . . 4 |- x e. V
32biantru 721 . . 3 |- (x = A <-> (x = A /\ x e. V))
43exbii 1027 . 2 |- (E.x x = A <-> E.x(x = A /\ x e. V))
51, 4bitr4 176 1 |- (A e. V <-> E.x x = A)
Colors of variables: wff set class
Syntax hints:   <-> wb 146   /\ wa 223  E.wex 956   = wceq 1099   e. wcel 1105  Vcvv 1786
This theorem is referenced by:  isseti 1790  issetri 1791  elisset 1792  elex 1794  vtoclgf 1821  cla4gf 1835  ceqex 1858  eueq 1888  moeq 1892  ru 1909  elrabsf 1934  snprc 2414  nvelv 2681  vnex 2683  dmsnop 3285  funimaexg 3515  isarep2 3518  fopab2 3762  tz9.12lem1 4583  tz9.12lem3 4585
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104  ax-17 1190  ax-ext 1436
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787
Copyright terms: Public domain