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 }