| 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 3461, without using ax-ext 2737. Note that this theorem has no
disjoint variable condition and does not use df-clel 2840 nor df-cleq 2757
either: only propositional logic and ax-gen 1828 and df-clab 2744. This is
sbt 2103 expressed using class abstractions.
Without ax-ext 2737, one cannot define "the" universal
class, since one
could not prove for instance the justification theorem
{𝑥
∣ ⊤} = {𝑦
∣ ⊤} (see vjust 3458). Indeed, in order to prove
any equality of classes, one needs df-cleq 2757, which has ax-ext 2737 as a
hypothesis. Therefore, the classes {𝑥 ∣ ⊤},
{𝑦
∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and
countless others are all universal classes whose equality cannot be
proved without ax-ext 2737. Once dfcleq 2758 is available, we will define
"the" universal class in df-v 3459.
Its degenerate instance is also a simple consequence of abid 2747
(using
mpbir 234). (Contributed by BJ, 13-Jun-2019.) Reduce
axiom
dependencies. (Revised by Steven Nguyen,
25-Apr-2023.) |
