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

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