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

Metamath Proof Explorer

Theorem rspesbca

Description: Existence form of rspsbca . (Contributed by NM, 29-Feb-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion rspesbca ⊢ A ∈ B ∧ [˙A / x]˙ φ → ∃ x ∈ B φ

Proof

Step Hyp Ref Expression
1 dfsbcq2 ⊢ y = A → y x φ ↔ [˙A / x]˙ φ
2 1 rspcev ⊢ A ∈ B ∧ [˙A / x]˙ φ → ∃ y ∈ B y x φ
3 cbvrexsvw ⊢ ∃ x ∈ B φ ↔ ∃ y ∈ B y x φ
4 2 3 sylibr ⊢ A ∈ B ∧ [˙A / x]˙ φ → ∃ x ∈ B φ