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

Metamath Proof Explorer

Theorem rsp3

Description: From a restricted universal statement over A , specialize to an arbitrary element y e. A , cf. rsp . (Contributed by Peter Mazsa, 9-Feb-2026)

Ref Expression
Hypotheses rsp3.1 ⊢ Ⅎ _ x A
rsp3.2 ⊢ Ⅎ _ y A
rsp3.3 ⊢ Ⅎ y φ
rsp3.4 ⊢ Ⅎ x ψ
rsp3.5 ⊢ x = y → φ ↔ ψ
Assertion rsp3 ⊢ ∀ x ∈ A φ → y ∈ A → ψ

Proof

Step Hyp Ref Expression
1 rsp3.1 ⊢ Ⅎ _ x A
2 rsp3.2 ⊢ Ⅎ _ y A
3 rsp3.3 ⊢ Ⅎ y φ
4 rsp3.4 ⊢ Ⅎ x ψ
5 rsp3.5 ⊢ x = y → φ ↔ ψ
6 1 2 3 4 5 cbvralfw ⊢ ∀ x ∈ A φ ↔ ∀ y ∈ A ψ
7 rsp ⊢ ∀ y ∈ A ψ → y ∈ A → ψ
8 6 7 sylbi ⊢ ∀ x ∈ A φ → y ∈ A → ψ