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

Metamath Proof Explorer

Theorem 19.3

Description: A wff may be quantified with a variable not free in it. Version of 19.9 with a universal quantifier. Theorem 19.3 of Margaris p. 89. See 19.3v for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993) (Revised by Mario Carneiro, 24-Sep-2016)

		Ref	Expression
	Hypothesis	19.3.1	⊢ Ⅎ 𝑥 𝜑
	Assertion	19.3	⊢ ( ∀ 𝑥 𝜑 ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		19.3.1	⊢ Ⅎ 𝑥 𝜑
2		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
3	1	nf5ri	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
4	2 3	impbii	⊢ ( ∀ 𝑥 𝜑 ↔ 𝜑 )