Theorem bj-hbext

Description: Closed form of bj-hbex and hbex . (Contributed by BJ, 10-Oct-2019)

	Ref	Expression
Assertion	bj-hbext	|- ( A. y A. x ( ph -> A. x ps ) -> ( E. y ph -> A. x E. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A. y A. x ( ph -> A. x ps ) -> A. y A. x ( ph -> A. x ps ) )
2		sp	|- ( A. x ( ph -> A. x ps ) -> ( ph -> A. x ps ) )
3	1 2	bj-hbexd	|- ( A. y A. x ( ph -> A. x ps ) -> ( E. y ph -> A. x E. y ps ) )