Description: Two ways to express that " A is a set": A class A is a member of the universal class _V (see df-v ) 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.
A class A which is not a set is called aproper class.
Conventions: We will often use the expression " A e.V " to mean " A is a set", for example in uniex . To make some theorems more readily applicable, we will also use the more general expression A e. V instead of A e. V to mean " A is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg compared with uniex ). That this is more general is seen either by substitution (when the variable V has no other occurrences), or by elex . (Contributed by NM, 26-May-1993)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isset | |- ( A e. _V <-> E. x x = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfclel | |- ( A e. _V <-> E. x ( x = A /\ x e. _V ) ) |
|
| 2 | vex | |- x e. _V |
|
| 3 | 2 | biantru | |- ( x = A <-> ( x = A /\ x e. _V ) ) |
| 4 | 3 | exbii | |- ( E. x x = A <-> E. x ( x = A /\ x e. _V ) ) |
| 5 | 1 4 | bitr4i | |- ( A e. _V <-> E. x x = A ) |