Description: This would be the justification theorem for the definition of the unary predicate "E!" by |- ( E! A <-> E. x x = A ) which could be interpreted as " A exists" (as a set) or " A denotes" (in the sense of free logic).
A shorter proof using bitri (to add an intermediate proposition E. z z = A with a fresh z ), cbvexvw , and eqeq1 , requires the core axioms and { ax-9 , ax-ext , df-cleq } whereas this proof requires the core axioms and { ax-8 , df-clab , df-clel }.
Theorem bj-issetwt proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 , df-clab , df-clel } (whereas with the shorter proof from cbvexvw and eqeq1 it would require { ax-8 , ax-9 , ax-ext , df-clab , df-cleq , df-clel }). That every class is equal to a class abstraction is proved by abid1 , which requires { ax-8 , ax-9 , ax-ext , df-clab , df-cleq , df-clel }.
Note that there is no disjoint variable condition on x , y but the theorem does not depend on ax-13 . Actually, the proof depends only on the logical axioms ax-1 through ax-7 and sp .
The symbol "E!" was chosen to be reminiscent of the analogous predicate in (inclusive or non-inclusive) free logic, which deals with the possibility of nonexistent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: these are derived from ax-ext and df-cleq (e.g., eqid and eqeq1 ). In particular, one cannot even prove |- E. x x = A => |- A = A without ax-ext and df-cleq .
(Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-denotes | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-denoteslem | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ { 𝑧 ∣ ⊤ } ) | |
| 2 | bj-denoteslem | ⊢ ( ∃ 𝑦 𝑦 = 𝐴 ↔ 𝐴 ∈ { 𝑧 ∣ ⊤ } ) | |
| 3 | 1 2 | bitr4i | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) |