Theorem bj-dfnnf3

Description: Alternate definition of nonfreeness when sp is available. (Contributed by BJ, 28-Jul-2023) The proof should not rely on df-nf . (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bj-nnfea	|- ( F// x ph -> ( E. x ph -> A. x ph ) )
2		bj-19.21bit	|- ( ( E. x ph -> A. x ph ) -> ( E. x ph -> ph ) )
3		bj-19.23bit	|- ( ( E. x ph -> A. x ph ) -> ( ph -> A. x ph ) )
4		df-bj-nnf	|- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
5	2 3 4	sylanbrc	|- ( ( E. x ph -> A. x ph ) -> F// x ph )
6	1 5	impbii	|- ( F// x ph <-> ( E. x ph -> A. x ph ) )