Description: If  is a theorem, then any set belongs to
the class
    .
Therefore, is
"a" universal class.
This is the closest one can get to defining a universal class, or
proving vex 3203, without using ax-ext 2602. Note that this theorem has no
dv condition and does not use df-clel 2618 nor df-cleq 2615 either: only
first-order logic and df-clab 2609.
Without ax-ext 2602, one cannot define "the" universal
class, since one
could not prove for instance the justification theorem
   (see vjust 3201). Indeed, in order to prove
any equality of classes, one needs df-cleq 2615, which has ax-ext 2602 as a
hypothesis. Therefore, the classes ,
   ,   
and
countless others are all universal classes whose equality one cannot
prove without ax-ext 2602. See also bj-issetw 32860.
A version with a dv condition between and and not requiring
ax-13 2246 is proved as bj-vexwv 32857, while the degenerate instance is a
simple consequence of abid 2610. (Contributed by BJ, 13-Jun-2019.)
(Proof modification is discouraged.) Use bj-vexwv 32857 instead when
sufficient. (New usage is discouraged.) |
