Description: Two ways to say " 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.Notational convention: We will use the notational device " A e.V " to mean " A is a set" very frequently, for example in uniex . Note that a class A which is not a set is called a proper class_. In some theorems, such as uniexg , in order to shorten certain proofs we use the more general antecedent A e. V instead of A e.V to mean " A is a set."
Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel requires that the expression substituted for B not contain x . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isset | ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfclel | ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) ) | |
| 2 | vex | ⊢ 𝑥 ∈ V | |
| 3 | 2 | biantru | ⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) ) |
| 4 | 3 | exbii | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) ) |
| 5 | 1 4 | bitr4i | ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 ) |