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 33187
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.)

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 33186 . . . . 5 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
32biantru 519 . . . 4 (𝑥 = 𝐴 ↔ (𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
43exbii 1924 . . 3 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
5 df-clel 2767 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
6 df-clel 2767 . . 3 (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
74, 5, 63bitr2i 288 . 2 (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
81bj-vexwv 33186 . . . . 5 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}
98biantru 519 . . . 4 (𝑦 = 𝐴 ↔ (𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}))
109bicomi 214 . . 3 ((𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴)
1110exbii 1924 . 2 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴)
127, 11bitri 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