Theorem abv

Description: The class of sets verifying a property is the universal class if and only if that property is a tautology. The reverse implication ( bj-abv ) requires fewer axioms. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (Proof shortened by BJ, 30-Aug-2024)

	Ref	Expression
Assertion	abv	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢\left\{x|\phi \right\}=\left\{x|\top \right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
2		vextru	$$⊢y\in \left\{x|\top \right\}$$
3	2	tbt	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
4		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
5	3 4	bitr3i	$$⊢\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)\leftrightarrow \left[y/x\right]\phi$$
6	5	albii	$$⊢\forall y\left(y\in \left\{x|\phi \right\}\leftrightarrow y\in \left\{x|\top \right\}\right)\leftrightarrow \forall y\left[y/x\right]\phi$$
7	1 6	bitri	$$⊢\left\{x|\phi \right\}=\left\{x|\top \right\}\leftrightarrow \forall y\left[y/x\right]\phi$$
8		dfv2	$$⊢\mathrm{V}=\left\{x|\top \right\}$$
9	8	eqeq2i	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \left\{x|\phi \right\}=\left\{x|\top \right\}$$
10		sb8v	$$⊢\forall x\phi \leftrightarrow \forall y\left[y/x\right]\phi$$
11	7 9 10	3bitr4i	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \forall x\phi$$