Theorem bj-hbext

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

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

Proof

Step	Hyp	Ref	Expression
1		nfa2	|- F/ x A. y A. x ( ph -> A. x ph )
2		hbnt	|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
3	2	alimi	|- ( A. y A. x ( ph -> A. x ph ) -> A. y ( -. ph -> A. x -. ph ) )
4		bj-hbalt	|- ( A. y ( -. ph -> A. x -. ph ) -> ( A. y -. ph -> A. x A. y -. ph ) )
5	3 4	syl	|- ( A. y A. x ( ph -> A. x ph ) -> ( A. y -. ph -> A. x A. y -. ph ) )
6	1 5	alrimi	|- ( A. y A. x ( ph -> A. x ph ) -> A. x ( A. y -. ph -> A. x A. y -. ph ) )
7		hbnt	|- ( A. x ( A. y -. ph -> A. x A. y -. ph ) -> ( -. A. y -. ph -> A. x -. A. y -. ph ) )
8	6 7	syl	|- ( A. y A. x ( ph -> A. x ph ) -> ( -. A. y -. ph -> A. x -. A. y -. ph ) )
9		df-ex	|- ( E. y ph <-> -. A. y -. ph )
10	9	bicomi	|- ( -. A. y -. ph <-> E. y ph )
11	10	albii	|- ( A. x -. A. y -. ph <-> A. x E. y ph )
12	8 10 11	3imtr3g	|- ( A. y A. x ( ph -> A. x ph ) -> ( E. y ph -> A. x E. y ph ) )