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.

Step	Hyp	Ref	Expression
1		id 22	. . . . . 6 ⊢ (𝑧 = 𝑧 → 𝑧 = 𝑧)
2	1	bj-vexwv 32051	. . . . 5 ⊢ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}
3	2	biantru 525	. . . 4 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
4	3	exbii 1764	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
5		df-clel 2606	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
6		df-clel 2606	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
7	4, 5, 6	3bitr2i 287	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
8	1	bj-vexwv 32051	. . . . 5 ⊢ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}
9	8	biantru 525	. . . 4 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}))
10	9	bicomi 213	. . 3 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ 𝑦 = 𝐴)
11	10	exbii 1764	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ (𝑧 = 𝑧 → 𝑧 = 𝑧)}) ↔ ∃𝑦 𝑦 = 𝐴)
12	7, 11	bitri 263	1 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)

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