MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vexw Structured version   Visualization version   GIF version

Theorem vexw 2809
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 3502, without using ax-ext 2797. Note that this theorem has no disjoint variable condition and does not use df-clel 2897 nor df-cleq 2818 either: only propositional logic and ax-gen 1789 and df-clab 2804. This is sbt 2064 expressed using class abstractions.

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

Its degenerate instance is also a simple consequence of abid 2807 (using mpbir 232). (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
StepHypRef Expression
1 vexw.1 . . 3 𝜑
21sbt 2064 . 2 [𝑦 / 𝑥]𝜑
3 df-clab 2804 . 2 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
42, 3mpbir 232 1 𝑦 ∈ {𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  [wsb 2062  wcel 2107  {cab 2803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789
This theorem depends on definitions:  df-bi 208  df-sb 2063  df-clab 2804
This theorem is referenced by:  vextru  2810  vex  3502  bj-denotes  34072  bj-ralvw  34079  bj-rexvw  34080  bj-rababw  34081  bj-df-v  34228
  Copyright terms: Public domain W3C validator