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 theorem for the definition of the unary
predicate "E!" by ⊢ ( E! 𝐴 ↔ ∃𝑥𝑥 = 𝐴) which could be
interpreted as "𝐴 exists" or "𝐴
denotes". It is interesting
that this justification theorem can be proved without ax-ext 2754 nor
df-cleq 2770 (but then one requires df-clab 2764 and df-clel 2774). The next
theorem bj-issetwt 33429 will prove that "existing" (as a
set) is equivalent
to being a member of a class abstraction (that every class is equal to a
class abstration is then proved by abid1 2911 / bj-termab , which requires
more axioms, including ax-ext 2754 and the three class related
definitions).
Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2334. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2055 and sp 2167. 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 2754 and df-cleq 2770 (e.g., eqid 2778 and eqeq1 2782). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2754 and df-cleq 2770. See also bj-denotesv 33428 and comments there. (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 33426 | . . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
3 | 2 | biantru 525 | . . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
4 | 3 | exbii 1892 | . . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
5 | df-clel 2774 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
6 | df-clel 2774 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) | |
7 | 4, 5, 6 | 3bitr2i 291 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
8 | 1 | bj-vexwv 33426 | . . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} |
9 | 8 | biantru 525 | . . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)})) |
10 | 9 | bicomi 216 | . . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴) |
11 | 10 | exbii 1892 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴) |
12 | 7, 11 | bitri 267 | 1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∃wex 1823 ∈ wcel 2107 {cab 2763 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-12 2163 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-sb 2012 df-clab 2764 df-clel 2774 |
This theorem is referenced by: bj-issetwt 33429 bj-elisset 33432 bj-vtoclg1f1 33482 |
Copyright terms: Public domain | W3C validator |