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 ⊢ Ⅎ x φ
Assertion ra4 ⊢ ∀ x ∈ A φ → ψ → φ → ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ra4.1 ⊢ Ⅎ x φ
2 1 r19.21 ⊢ ∀ x ∈ A φ → ψ ↔ φ → ∀ x ∈ A ψ
3 2 biimpi ⊢ ∀ x ∈ A φ → ψ → φ → ∀ x ∈ A ψ