Metamath Proof Explorer

Theorem rspct

Description: A closed version of rspc . (Contributed by Andrew Salmon, 6-Jun-2011)

Ref Expression
Hypothesis rspct.1 ⊢ Ⅎ x ψ
Assertion rspct ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → ∀ x ∈ B φ → ψ

Proof

Step Hyp Ref Expression
1 rspct.1 ⊢ Ⅎ x ψ
2 df-ral ⊢ ∀ x ∈ B φ ↔ ∀ x x ∈ B → φ
3 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
4 3 adantr ⊢ x = A ∧ φ ↔ ψ → x ∈ B ↔ A ∈ B
5 simpr ⊢ x = A ∧ φ ↔ ψ → φ ↔ ψ
6 4 5 imbi12d ⊢ x = A ∧ φ ↔ ψ → x ∈ B → φ ↔ A ∈ B → ψ
7 6 ex ⊢ x = A → φ ↔ ψ → x ∈ B → φ ↔ A ∈ B → ψ
8 7 a2i ⊢ x = A → φ ↔ ψ → x = A → x ∈ B → φ ↔ A ∈ B → ψ
9 8 alimi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x x = A → x ∈ B → φ ↔ A ∈ B → ψ
10 nfv ⊢ Ⅎ x A ∈ B
11 10 1 nfim ⊢ Ⅎ x A ∈ B → ψ
12 nfcv ⊢ Ⅎ _ x A
13 11 12 spcgft ⊢ ∀ x x = A → x ∈ B → φ ↔ A ∈ B → ψ → A ∈ B → ∀ x x ∈ B → φ → A ∈ B → ψ
14 9 13 syl ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → ∀ x x ∈ B → φ → A ∈ B → ψ
15 2 14 syl7bi ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → ∀ x ∈ B φ → A ∈ B → ψ
16 15 com34 ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → A ∈ B → ∀ x ∈ B φ → ψ
17 16 pm2.43d ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → ∀ x ∈ B φ → ψ