Theorem r19.3rz

Description: Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008)

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

Proof

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