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

Metamath Proof Explorer

Theorem ra4

Description: Restricted quantifier version of Axiom 5 of Mendelson p. 69. This is the axiom stdpc5 of standard predicate calculus for a restricted domain. See ra4v for a version requiring fewer axioms. (Contributed by NM, 16-Jan-2004) (Proof shortened by BJ, 27-Mar-2020)

		Ref	Expression
	Hypothesis	ra4.1	⊢ Ⅎ 𝑥 𝜑
	Assertion	ra4	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ra4.1	⊢ Ⅎ 𝑥 𝜑
2	1	r19.21	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )
3	2	biimpi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )