Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-denotes Structured version   Visualization version   GIF version

Theorem bj-denotes 32505
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.)

Assertion
Ref Expression
bj-denotes (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Proof of Theorem bj-denotes
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . 6 (𝑧 = 𝑧𝑧 = 𝑧)
21bj-vexwv 32504 . . . . 5 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
32biantru 526 . . . 4 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
43exbii 1771 . . 3 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
5 df-clel 2617 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
6 df-clel 2617 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
74, 5, 63bitr2i 288 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
81bj-vexwv 32504 . . . . 5 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
98biantru 526 . . . 4 (𝑦 = 𝐴 ↔ (𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
109bicomi 214 . . 3 ((𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴)
1110exbii 1771 . 2 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴)
127, 11bitri 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