This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )