Metamath Proof Explorer

Theorem rspce

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Revised by Mario Carneiro, 11-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 rspc.1 ⊢ Ⅎ x ψ
2 rspc.2 ⊢ x = A → φ ↔ ψ
3 nfcv ⊢ Ⅎ _ x A
4 nfv ⊢ Ⅎ x A ∈ B
5 4 1 nfan ⊢ Ⅎ x A ∈ B ∧ ψ
6 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
7 6 2 anbi12d ⊢ x = A → x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
8 3 5 7 spcegf ⊢ A ∈ B → A ∈ B ∧ ψ → ∃ x x ∈ B ∧ φ
9 8 anabsi5 ⊢ A ∈ B ∧ ψ → ∃ x x ∈ B ∧ φ
10 df-rex ⊢ ∃ x ∈ B φ ↔ ∃ x x ∈ B ∧ φ
11 9 10 sylibr ⊢ A ∈ B ∧ ψ → ∃ x ∈ B φ