**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 2419 nor df-cleq 2433
(but of course using df-clab 2427 and df-clel 2436). Once extensionality is
postulated, then isset 3097 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 1983. Actually, the proof depends only on ax-1--7
and
sp 1843.
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 2419 (e.g. eqid 2441). In particular, one cannot even
prove
.
With ax-ext 2419, the present theorem is obvious from cbvexv 2008 and eqeq1 2445
(in free logic, the same proof holds since one has equality axioms for
terms). (Contributed by BJ, 29-Apr-2019.)
(Proof modification is discouraged.) |