Metamath Proof Explorer


Theorem vexw

Description: If ph is a theorem, then any set belongs to the class { x | ph } . Therefore, { x | ph } is "a" universal class.

This is the closest one can get to defining a universal class, or proving vex , without using ax-ext . Note that this theorem has no disjoint variable condition and does not use df-clel nor df-cleq either: only propositional logic and ax-gen and df-clab . This is sbt expressed using class abstractions.

Without ax-ext , one cannot define "the" universal class, since one could not prove for instance the justification theorem { x | T. } = { y | T. } (see vjust ). Indeed, in order to prove any equality of classes, one needs df-cleq , which has ax-ext as a hypothesis. Therefore, the classes { x | T. } , { y | ( ph -> ph ) } , { z | ( A. t t = t -> A. t t = t ) } and countless others are all universal classes whose equality cannot be proved without ax-ext . Once dfcleq is available, we will define "the" universal class in df-v .

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

Ref Expression
Hypothesis vexw.1
|- ph
Assertion vexw
|- y e. { x | ph }

Proof

Step Hyp Ref Expression
1 vexw.1
 |-  ph
2 1 sbt
 |-  [ y / x ] ph
3 df-clab
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
4 2 3 mpbir
 |-  y e. { x | ph }