Theorem r19.3rzf

Description: Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	r19.3rzf.1	⊢ Ⅎ 𝑥 𝜑
	r19.3rzf.2	⊢ Ⅎ 𝑥 𝐴
Assertion	r19.3rzf	⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.3rzf.1	⊢ Ⅎ 𝑥 𝜑
2		r19.3rzf.2	⊢ Ⅎ 𝑥 𝐴
3	2	n0f	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
4		biimt	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( 𝜑 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝜑 ) ) )
5	3 4	sylbi	⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝜑 ) ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
7	1	19.23	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝜑 ) )
8	6 7	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝜑 ) )
9	5 8	bitr4di	⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )