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	⊢ ( Ⅎ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.38	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
2		exim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
3		id	⊢ ( Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 𝜓 )
4	3	nfrd	⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
5	2 4	syl9r	⊢ ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) )
6	1 5	impbid2	⊢ ( Ⅎ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )