Metamath Proof Explorer

Theorem bj-nnfe

Description: Nonfreeness implies the equivalent of ax5e . (Contributed by BJ, 28-Jul-2023)

Ref Expression
Assertion bj-nnfe 
|- ( F// x ph -> ( E. x ph -> ph ) )

Proof

Step Hyp Ref Expression
1 df-bj-nnf 
 |-  ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
2 1 simplbi 
 |-  ( F// x ph -> ( E. x ph -> ph ) )