Metamath Proof Explorer


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