Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-denotes | Structured version Visualization version GIF version |
Description: This would be the
justification for the definition of the unary
predicate "E!" by ⊢ ( E! 𝐴 ↔ ∃𝑥𝑥 = 𝐴) which could be
interpreted as "𝐴 exists" or "𝐴
denotes". It is interesting
that this justification can be proved without ax-ext 2601 nor df-cleq 2614
(but of course using df-clab 2608 and df-clel 2617). Once extensionality is
postulated, then isset 3193 will prove that "existing" (as a
set) is
equivalent to being a member of a class.
Note that there is no dv condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2245. Actually, the proof depends only on ax-1--7 and sp 2051. 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 non-existent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: they are derived from ax-ext 2601 (e.g., eqid 2621). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴. With ax-ext 2601, the present theorem is obvious from cbvexv 2274 and eqeq1 2625 (in free logic, the same proof holds since one has equality axioms for terms). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-denotes | ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . . . . 6 ⊢ (𝑧 = 𝑧 → 𝑧 = 𝑧) | |
2 | 1 | bj-vexwv 32504 | . . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
3 | 2 | biantru 526 | . . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
4 | 3 | exbii 1771 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
5 | df-clel 2617 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
6 | df-clel 2617 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
7 | 4, 5, 6 | 3bitr2i 288 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
8 | 1 | bj-vexwv 32504 | . . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
9 | 8 | biantru 526 | . . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
10 | 9 | bicomi 214 | . . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴) |
11 | 10 | exbii 1771 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴) |
12 | 7, 11 | bitri 264 | 1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1480 ∃wex 1701 ∈ wcel 1987 {cab 2607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-12 2044 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1702 df-sb 1878 df-clab 2608 df-clel 2617 |
This theorem is referenced by: bj-issetwt 32506 bj-elisset 32509 bj-vtoclg1f1 32557 |
Copyright terms: Public domain | W3C validator |