Metamath Proof Explorer

Theorem bj-nnfext

Description: See nfex and bj-nfext . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfext 
|- ( A. x F// y ph -> F// y E. x ph )

Proof

Step Hyp Ref Expression
1 df-bj-nnf 
 |-  ( F// y ph <-> ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) )
2 1 albii 
 |-  ( A. x F// y ph <-> A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) )
3 simpl 
 |-  ( ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( E. y ph -> ph ) )
4 3 alimi 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> A. x ( E. y ph -> ph ) )
5 bj-nnflemee 
 |-  ( A. x ( E. y ph -> ph ) -> ( E. y E. x ph -> E. x ph ) )
6 4 5 syl 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( E. y E. x ph -> E. x ph ) )
7 2 6 sylbi 
 |-  ( A. x F// y ph -> ( E. y E. x ph -> E. x ph ) )
8 simpr 
 |-  ( ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( ph -> A. y ph ) )
9 8 alimi 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> A. x ( ph -> A. y ph ) )
10 bj-nnflemae 
 |-  ( A. x ( ph -> A. y ph ) -> ( E. x ph -> A. y E. x ph ) )
11 9 10 syl 
 |-  ( A. x ( ( E. y ph -> ph ) /\ ( ph -> A. y ph ) ) -> ( E. x ph -> A. y E. x ph ) )
12 2 11 sylbi 
 |-  ( A. x F// y ph -> ( E. x ph -> A. y E. x ph ) )
13 df-bj-nnf 
 |-  ( F// y E. x ph <-> ( ( E. y E. x ph -> E. x ph ) /\ ( E. x ph -> A. y E. x ph ) ) )
14 7 12 13 sylanbrc 
 |-  ( A. x F// y ph -> F// y E. x ph )