Theorem vexw 2782

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 3444, without using ax-ext 2770. Note that this theorem has no disjoint variable condition and does not use df-clel 2870 nor df-cleq 2791 either: only propositional logic and ax-gen 1797 and df-clab 2777. This is sbt 2071 expressed using class abstractions.

Without ax-ext 2770, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3442). Indeed, in order to prove any equality of classes, one needs df-cleq 2791, which has ax-ext 2770 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality cannot be proved without ax-ext 2770. Once dfcleq 2792 is available, we will define "the" universal class in df-v 3443.

Its degenerate instance is also a simple consequence of abid 2780 (using mpbir 234). (Contributed by BJ, 13-Jun-2019.) Reduce axiom dependencies. (Revised by Steven Nguyen, 25-Apr-2023.)

Hypothesis

Ref	Expression
vexw.1	⊢ 𝜑

Assertion

Ref	Expression
vexw	⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}

Proof of Theorem vexw

Step	Hyp	Ref	Expression
1		vexw.1	. . 3 ⊢ 𝜑
2	1	sbt 2071	. 2 ⊢ [𝑦 / 𝑥]𝜑
3		df-clab 2777	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4	2, 3	mpbir 234	1 ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}

Syntax hints:  [wsb 2069   ∈ wcel 2111  {cab 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797

This theorem depends on definitions:  df-bi 210  df-sb 2070  df-clab 2777

This theorem is referenced by:  vextru  2783  vex  3444  bj-ralvw  34319  bj-rexvw  34320  bj-rababw  34321  bj-df-v  34471