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 2590 nor df-cleq 2603
(but of course using df-clab 2597 and df-clel 2606). Once extensionality is
postulated, then isset 3180 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 2234. Actually, the proof depends only on ax-1--7 and sp 2041. 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 2590 (e.g., eqid 2610). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴. With ax-ext 2590, the present theorem is obvious from cbvexv 2263 and eqeq1 2614 (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 32051 | . . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
3 | 2 | biantru 525 | . . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
4 | 3 | exbii 1764 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
5 | df-clel 2606 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
6 | df-clel 2606 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
7 | 4, 5, 6 | 3bitr2i 287 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
8 | 1 | bj-vexwv 32051 | . . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
9 | 8 | biantru 525 | . . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
10 | 9 | bicomi 213 | . . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴) |
11 | 10 | exbii 1764 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴) |
12 | 7, 11 | bitri 263 | 1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-sb 1868 df-clab 2597 df-clel 2606 |
This theorem is referenced by: bj-issetwt 32053 bj-elisset 32056 bj-vtoclg1f1 32102 |
Copyright terms: Public domain | W3C validator |