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 2751 nor df-cleq 2764
(but of course using df-clab 2758 and df-clel 2767). Once extensionality is
postulated, then isset 3359 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 2408. Actually, the proof depends only on ax-1--7 and sp 2207. 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 2751 (e.g., eqid 2771). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴. With ax-ext 2751, the present theorem is obvious from cbvexv 2435 and eqeq1 2775 (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 33186 | . . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
3 | 2 | biantru 519 | . . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
4 | 3 | exbii 1924 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
5 | df-clel 2767 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
6 | df-clel 2767 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
7 | 4, 5, 6 | 3bitr2i 288 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
8 | 1 | bj-vexwv 33186 | . . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
9 | 8 | biantru 519 | . . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
10 | 9 | bicomi 214 | . . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴) |
11 | 10 | exbii 1924 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴) |
12 | 7, 11 | bitri 264 | 1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ∃wex 1852 ∈ wcel 2145 {cab 2757 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-sb 2050 df-clab 2758 df-clel 2767 |
This theorem is referenced by: bj-issetwt 33188 bj-elisset 33191 bj-vtoclg1f1 33240 |
Copyright terms: Public domain | W3C validator |