Theorem bj-denotes

Description: This would be the justification theorem for the definition of the unary predicate "E!" by |- ( E! A <-> E. x x = A ) which could be interpreted as " A exists" (as a set) or " A denotes" (in the sense of free logic).

A shorter proof using bitri (to add an intermediate proposition E. z z = A with a fresh z ), cbvexvw , and eqeq1 , requires the core axioms and { ax-9 , ax-ext , df-cleq } whereas this proof requires the core axioms and { ax-8 , df-clab , df-clel }.

Theorem bj-issetwt proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 , df-clab , df-clel } (whereas with the shorter proof from cbvexvw and eqeq1 it would require { ax-8 , ax-9 , ax-ext , df-clab , df-cleq , df-clel }). That every class is equal to a class abstraction is proved by abid1 , which requires { ax-8 , ax-9 , ax-ext , df-clab , df-cleq , df-clel }.

Note that there is no disjoint variable condition on x , y but the theorem does not depend on ax-13 . Actually, the proof depends only on the logical axioms ax-1 through ax-7 and sp .

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 and df-cleq (e.g., eqid and eqeq1 ). In particular, one cannot even prove |- E. x x = A => |- A = A without ax-ext and df-cleq .

(Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-denotes	|- ( E. x x = A <-> E. y y = A )

Proof

Step	Hyp	Ref	Expression
1		bj-denoteslem	|- ( E. x x = A <-> A e. { z | T. } )
2		bj-denoteslem	|- ( E. y y = A <-> A e. { z | T. } )
3	1 2	bitr4i	|- ( E. x x = A <-> E. y y = A )