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 32052
 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.)
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 32051 . . . . 5 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
32biantru 525 . . . 4 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
43exbii 1764 . . 3 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
5 df-clel 2606 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
6 df-clel 2606 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
74, 5, 63bitr2i 287 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
81bj-vexwv 32051 . . . . 5 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
98biantru 525 . . . 4 (𝑦 = 𝐴 ↔ (𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
109bicomi 213 . . 3 ((𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴)
1110exbii 1764 . 2 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴)
127, 11bitri 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