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.

Step	Hyp	Ref	Expression
1		id 22	. . . . . 6 ⊢ (𝑧 = 𝑧 → 𝑧 = 𝑧)
2	1	bj-vexwv 33426	. . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}
3	2	biantru 525	. . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
4	3	exbii 1892	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
5		df-clel 2774	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
6		df-clel 2774	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
7	4, 5, 6	3bitr2i 291	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
8	1	bj-vexwv 33426	. . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}
9	8	biantru 525	. . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
10	9	bicomi 216	. . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴)
11	10	exbii 1892	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴)
12	7, 11	bitri 267	1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)

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