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 GG, 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		sb8v	\|- ( A. x ph <-> A. y [ y / x ] ph )
11	7 9 10	3bitr4i	\|- ( { x \| ph } = _V <-> A. x ph )

Metamath Proof Explorer

Theorem abv

Proof