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

Metamath Proof Explorer

Theorem rspsbc

Description: Restricted quantifier version of Axiom 4 of Mendelson p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 and spsbc . See also rspsbca and rspcsbela . (Contributed by NM, 17-Nov-2006) (Proof shortened by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion rspsbc ⊢ A ∈ B → ∀ x ∈ B φ → [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 cbvralsvw ⊢ ∀ x ∈ B φ ↔ ∀ y ∈ B y x φ
2 dfsbcq2 ⊢ y = A → y x φ ↔ [˙A / x]˙ φ
3 2 rspcv ⊢ A ∈ B → ∀ y ∈ B y x φ → [˙A / x]˙ φ
4 1 3 biimtrid ⊢ A ∈ B → ∀ x ∈ B φ → [˙A / x]˙ φ