**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 2438 nor df-cleq 2452
(but of course using df-clab 2446 and df-clel 2455). Once extensionality is
postulated, then isset 3110 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 1961. Actually, the proof depends only on ax-1--7
and
sp 1803.
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 2438 (e.g. eqid 2460). In particular, one cannot even
prove
.
With ax-ext 2438, the present theorem is obvious from cbvexv 1990 and eqeq1 2464
(in free logic, the same proof holds since one has equality axioms for
terms). (Contributed by BJ, 29-Apr-2019.)
(Proof modification is discouraged.) |