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

Metamath Proof Explorer

Theorem rspc

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)

Ref Expression
Hypotheses rspc.1 ⊢ Ⅎ x ψ
rspc.2 ⊢ x = A → φ ↔ ψ
Assertion rspc ⊢ A ∈ B → ∀ x ∈ B φ → ψ

Proof

Step Hyp Ref Expression
1 rspc.1 ⊢ Ⅎ x ψ
2 rspc.2 ⊢ x = A → φ ↔ ψ
3 df-ral ⊢ ∀ x ∈ B φ ↔ ∀ x x ∈ B → φ
4 nfcv ⊢ Ⅎ _ x A
5 nfv ⊢ Ⅎ x A ∈ B
6 5 1 nfim ⊢ Ⅎ x A ∈ B → ψ
7 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
8 7 2 imbi12d ⊢ x = A → x ∈ B → φ ↔ A ∈ B → ψ
9 4 6 8 spcgf ⊢ A ∈ B → ∀ x x ∈ B → φ → A ∈ B → ψ
10 9 pm2.43a ⊢ A ∈ B → ∀ x x ∈ B → φ → ψ
11 3 10 biimtrid ⊢ A ∈ B → ∀ x ∈ B φ → ψ