This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )