**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 3353, without using ax-ext 2743. Note that this theorem has no
disjoint variable condition and does not use df-clel 2761 nor df-cleq 2758
either: only first-order logic and df-clab 2752.
Without ax-ext 2743, one cannot define "the" universal
class, since one
could not prove for instance the justification theorem
{𝑥
∣ ⊤} = {𝑦
∣ ⊤} (see vjust 3351). Indeed, in order to prove
any equality of classes, one needs df-cleq 2758, which has ax-ext 2743 as a
hypothesis. Therefore, the classes {𝑥 ∣ ⊤},
{𝑦
∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and
countless others are all universal classes whose equality one cannot
prove without ax-ext 2743. See also bj-issetw 33285.
A version with a disjoint variable condition between 𝑥 and
𝑦
and
not requiring ax-13 2352 is proved as bj-vexwv 33281, while the degenerate
instance is a simple consequence of abid 2753.
(Contributed by BJ,
13-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwv 33281
instead when sufficient. (New usage is
discouraged.) |