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

Metamath Proof Explorer

Theorem rgen

Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994)

Ref Expression
Hypothesis rgen.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝜑 )
Assertion rgen ∀ 𝑥 ∈ 𝐴 𝜑

Proof

Step Hyp Ref Expression
1 rgen.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝜑 )
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3 2 1 mpgbir ⊢ ∀ 𝑥 ∈ 𝐴 𝜑