Theorem bj-abv

Description: The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-abv	|- ( A. x ph -> { x | ph } = _V )

Proof

Step	Hyp	Ref	Expression
1		trud	|- ( ( ph /\ ph ) -> T. )
2		simpl	|- ( ( ph /\ T. ) -> ph )
3	1 2	impbida	|- ( ph -> ( ph <-> T. ) )
4	3	alimi	|- ( A. x ph -> A. x ( ph <-> T. ) )
5		abbi1	|- ( A. x ( ph <-> T. ) -> { x | ph } = { x | T. } )
6	4 5	syl	|- ( A. x ph -> { x | ph } = { x | T. } )
7		dfv2	|- _V = { x | T. }
8	6 7	eqtr4di	|- ( A. x ph -> { x | ph } = _V )