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