Theorem abvALT

Description: Alternate proof of abv , shorter but using more axioms. (Contributed by BJ, 19-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
2	1	albii	|- ( A. y y e. { x | ph } <-> A. y [ y / x ] ph )
3		eqv	|- ( { x | ph } = _V <-> A. y y e. { x | ph } )
4		nfv	|- F/ y ph
5	4	sb8v	|- ( A. x ph <-> A. y [ y / x ] ph )
6	2 3 5	3bitr4i	|- ( { x | ph } = _V <-> A. x ph )