Metamath Proof Explorer

Theorem bj-nnfv

Description: A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023)

Ref Expression
Assertion bj-nnfv 
|- F// x ph

Proof

Step Hyp Ref Expression
1 ax5e 
 |-  ( E. x ph -> ph )
2 ax-5 
 |-  ( ph -> A. x ph )
3 df-bj-nnf 
 |-  ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
4 1 2 3 mpbir2an 
 |-  F// x ph