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

Metamath Proof Explorer

Theorem hbexg

Description: Closed form of nfex . Derived from hbexgVD . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 12-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfa2 
 |-  F/ y A. x A. y ( ph -> A. x ph )
2 sp 
 |-  ( A. y ( ph -> A. x ph ) -> ( ph -> A. x ph ) )
3 2 alimi 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. x ( ph -> A. x ph ) )
4 nf5 
 |-  ( F/ x ph <-> A. x ( ph -> A. x ph ) )
5 3 4 sylibr 
 |-  ( A. x A. y ( ph -> A. x ph ) -> F/ x ph )
6 1 5 nfexd 
 |-  ( A. x A. y ( ph -> A. x ph ) -> F/ x E. y ph )
7 nf5 
 |-  ( F/ x E. y ph <-> A. x ( E. y ph -> A. x E. y ph ) )
8 6 7 sylib 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. x ( E. y ph -> A. x E. y ph ) )
9 1 8 alrimi 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. y A. x ( E. y ph -> A. x E. y ph ) )
10 alcom 
 |-  ( A. y A. x ( E. y ph -> A. x E. y ph ) <-> A. x A. y ( E. y ph -> A. x E. y ph ) )
11 9 10 sylib 
 |-  ( A. x A. y ( ph -> A. x ph ) -> A. x A. y ( E. y ph -> A. x E. y ph ) )