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 2422 nor df-cleq 2434
(but of course using df-clab 2428 and df-clel 2437). Note that there is no
dv condition on . Once extensionality is
postulated, then
isset 2974 will prove that "existing" (as a
set) is equivalent to being a
member of a class.
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 2422 (e.g. eqid 2441). In particular, one cannot even
prove
.
With ax-ext 2422, the present theorem is obvious from cbvexv 1977 and eqeq1 2447
(in free logic, the same proof holds since one has equality axioms for
terms). (Contributed by BJ, 29-Apr-2019.)
(Proof modification is discouraged.) |