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	|- ( { x | ph } = _V <-> A. x ph )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( { x | ph } = { x | T. } <-> A. y ( y e. { x | ph } <-> y e. { x | T. } ) )
2		vextru	|- y e. { x | T. }
3	2	tbt	|- ( y e. { x | ph } <-> ( y e. { x | ph } <-> y e. { x | T. } ) )
4		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
5	3 4	bitr3i	|- ( ( y e. { x | ph } <-> y e. { x | T. } ) <-> [ y / x ] ph )
6	5	albii	|- ( A. y ( y e. { x | ph } <-> y e. { x | T. } ) <-> A. y [ y / x ] ph )
7	1 6	bitri	|- ( { x | ph } = { x | T. } <-> A. y [ y / x ] ph )
8		dfv2	|- _V = { x | T. }
9	8	eqeq2i	|- ( { x | ph } = _V <-> { x | ph } = { x | T. } )
10		nfv	|- F/ y ph
11	10	sb8v	|- ( A. x ph <-> A. y [ y / x ] ph )
12	7 9 11	3bitr4i	|- ( { x | ph } = _V <-> A. x ph )