Theorem 19.38b

Description: Under a non-freeness hypothesis, the implication 19.38 can be strengthened to an equivalence. See also 19.38a . (Contributed by BJ, 3-Nov-2021) (Proof shortened by Wolf Lammen, 9-Jul-2022)

	Ref	Expression
Assertion	19.38b	|- ( F/ x ps -> ( ( E. x ph -> A. x ps ) <-> A. x ( ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.38	|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
2		exim	|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
3		id	|- ( F/ x ps -> F/ x ps )
4	3	nfrd	|- ( F/ x ps -> ( E. x ps -> A. x ps ) )
5	2 4	syl9r	|- ( F/ x ps -> ( A. x ( ph -> ps ) -> ( E. x ph -> A. x ps ) ) )
6	1 5	impbid2	|- ( F/ x ps -> ( ( E. x ph -> A. x ps ) <-> A. x ( ph -> ps ) ) )